cert_inhabited
plain-language theorem explainer
The horizon-problem certificate type is inhabited: there is a concrete witness packing diagonal vanishing of domain cost, nonnegativity for positive masses and energies, and positivity of the canonical threshold. Cosmologists citing the RS 8-tick horizon resolution use this to discharge Nonempty obligations. The proof is a one-line term that packages the existing cert value.
Claim. The type of horizon-problem certificates is nonempty: there exists a record whose fields assert that the domain cost vanishes on the diagonal ($C(r,r)=0$ for $r\neq 0$), is nonnegative for positive arguments, and that the canonical threshold is strictly positive.
background
This module treats the cosmological horizon problem as a structural consequence of the Recognition Science 8-tick cadence and the J-cost. The module doc frames a structural theorem (zero sorry, zero axiom): inflation with $N_e=44$ e-folds at $T=J(\varphi),T_{\mathrm{Planck}}$ yields $\varphi^{44}\sim 10^9$ expansion, read as consistent with the classical $10^{24}$–$10^{26}$ requirement under the RS interpretation.
HorizonProb3Cert is a three-field certificate: domain cost equals zero when both arguments coincide and are nonzero; domain cost is nonnegative whenever both mass and energy arguments are positive; and the canonical threshold is positive. Domain cost is the local cost functional built from the RS J-cost (the unique cost forced by the Recognition Composition Law), specialized to the horizon-domain comparison.
The sibling cert is the concrete inhabitant of that structure; the present theorem only records that the type is nonempty.
proof idea
One-line term proof. The inhabitant is the already-constructed cert value, introduced via the anonymous constructor ⟨cert⟩ for Nonempty HorizonProb3Cert. No tactics, no further lemmas: the certificate fields were discharged upstream when cert was defined.
why it matters
In the RS cosmology stack this is the inhabitance seal for the Plan v7 horizon-problem certificate. It sits under the structural claim that the horizon problem is solved by 8-tick inflation with $N_e=44$ at temperature scaled by $J(\varphi)$, tying to the forcing-chain landmarks T5 (J-uniqueness), T6 ($\varphi$ fixed point), and T7 (eight-tick octave). No downstream users are recorded in the graph yet; the theorem exists so later cosmology lemmas can assume a nonempty certificate without re-proving the three field inequalities. It closes the local certificate interface rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.