cert_inhabited
plain-language theorem explainer
The matter-radiation equality certificate type is inhabited: there is a concrete witness packing diagonal vanishing of domain cost, nonnegativity for positive arguments, and positivity of the canonical threshold. Cosmology consumers that need a proof the module's cost axioms hold would cite this. Proof is a one-line term introducing the preexisting certificate value as the Nonempty witness.
Claim. The type of certificates for RS cosmology module 7 is nonempty: there exists a record asserting (i) domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ for all $r\neq 0$; (ii) domain cost is nonnegative for positive arguments; (iii) the canonical threshold is strictly positive.
background
Module 7 of the RS cosmology stack treats matter-radiation equality. The module claim is structural: $\phi^{17}\cdot 0.95$ yields $z_{\mathrm{eq}}\sim 3400$, matching the empirical equality redshift, with status "STRUCTURAL THEOREM (0 sorry, 0 axiom)".
The certificate structure packages three elementary properties used by that claim. Domain cost is the local two-argument cost on a matter/energy pair (J-cost style: zero on equal nonzero arguments, nonnegative when both arguments are positive). The canonical threshold is the positive scale against which the equality comparison is made.
Upstream, the structure itself only declares those three fields; inhabitation is what turns the interface into a proved bundle.
proof idea
One-line term proof. The module already constructs a value cert of type RSCosmo007Cert (filling the three fields from the sibling lemmas on diagonal vanishing, nonnegativity, and threshold positivity). The theorem is the standard Nonempty introduction: package that value as the witness $\langle\mathrm{cert}\rangle$.
why it matters
Closes the module's certificate interface: without inhabitation, the three cost/threshold properties remain a bare structure. With it, downstream cosmology code can assume a proved bundle rather than re-proving diagonal vanishing and nonnegativity at each use site.
No downstream dependents are recorded yet (used_by is empty), so the immediate role is module-level completeness for the matter-radiation equality structural theorem. In the broader RS stack this sits on the cosmology side of the phi-ladder (equality redshift near $\phi^{17}$), not on the T0-T8 forcing chain, RCL, or the alpha band. It does not itself compute $z_{\mathrm{eq}}$; it only certifies the cost axioms the module relies on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.