HorizonProb3Cert
plain-language theorem explainer
Certificate bundle of three elementary properties used in the RS horizon-problem argument from J-cost: diagonal domain cost vanishes, domain cost is nonnegative on positive arguments, and the canonical threshold is positive. Cosmology readers of the 8-tick inflation resolution cite this as the interface the later inhabitation proof fills. Pure structure definition; no proof body.
Claim. A horizon-problem certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats the classical cosmological horizon problem as resolved inside Recognition Science by an 8-tick inflation story: $N_e = 44$ e-folds at temperature $T = J(\varphi),T_{\mathrm{Planck}}$, with expansion factor $\varphi^{44}\sim 10^9$ (interpreted against the usual $10^{24}$–$10^{26}$ requirement). Status is structural: zero sorry, zero axiom.
Domain cost is the local cost functional on pairs of positive reals that the argument uses in place of a raw spacetime distance; the canonical threshold is the positive cutoff against which that cost is compared. Both sit downstream of the global J-cost calculus.
Upstream, nonnegativity of recognition-event cost is already forced: any recognition event has cost $\ge 0$ because $J$ is nonnegative on positive reals. The certificate simply re-exports the corresponding domain-level nonnegativity together with the diagonal-vanishing and threshold-positivity facts needed for the horizon comparison.
proof idea
No proof: this is a structure declaration whose three fields are propositions. Inhabitation is separate. The concrete witness later assigns the sibling lemmas for diagonal vanishing of domain cost, nonnegativity of domain cost on positive arguments, and positivity of the canonical threshold into those three fields.
why it matters
Gives the typed interface that the module's concrete certificate and the Nonempty inhabitation theorem fill, so downstream cosmology code can depend on a single named bundle rather than three loose lemmas.
In the RS forcing picture this sits under the 8-tick octave (T7) and the unique J-cost (T5): the horizon comparison is phrased entirely in J-derived domain cost and a positive threshold, not in an external inflation potential. The module doc frames the physical claim as $N_e=44$ e-folds at $T=J(\varphi)T_{\mathrm{Planck}}$.
It does not itself close the full horizon-problem derivation; it only packages the cost/threshold side conditions that derivation assumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.