cert_inhabited
plain-language theorem explainer
The RS Cosmology Module 3 certificate type is inhabited: there is a concrete pack of the domain-cost diagonal identity, nonnegativity, and positive canonical threshold. Cosmologists citing the structural Hubble-tension pass (H0_local/H0_CMB band containing SH0ES) use this existence fact. Proof is a one-line term that feeds the prebuilt certificate into the structure constructor.
Claim. The type of RS Cosmology Module 3 certificates is nonempty: there exists a record asserting 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
Module 3 is the structural Hubble-tension certificate in the RS cosmology stack. The module doc fixes the target band $H_{0,\mathrm{local}}/H_{0,\mathrm{CMB}}\in(1.075,1.091)$ with SH0ES $1.0837$ inside, and marks the file as a structural theorem (zero sorry, zero axiom) with status RS_PASS.
The certificate structure packages three elementary cost facts: domain cost equals zero when model and evidence coincide (off zero), domain cost is nonnegative on the positive quadrant, and the module's canonical threshold is positive. Domain cost is the local cost functional imported from the Cost layer (J-cost style comparison of two positive scales); the threshold is the positive cutoff used to gate the tension claim.
Upstream, the structure itself is only a Prop-bearing record; inhabitation is what turns the checklist into a proved certificate object.
proof idea
Term-mode one-liner. The proof is the anonymous constructor ⟨cert⟩, which supplies the already-defined concrete certificate value cert as the unique field witness for Nonempty RSCosmo003Cert. No tactics, no rewriting: pure inhabitation of the structure type.
why it matters
This is the existence seal for Cosmology Module 3's structural pass on the Hubble tension. The parent narrative is the module claim that the local-to-CMB $H_0$ ratio band $(1.075,1.091)$ contains the SH0ES point and is RS_PASS under the cost/threshold package. In the broader RS stack, such cert_inhabited lemmas turn cost-layer identities (diagonal vanishing and nonnegativity of the recognition cost, positive threshold) into exportable cosmology certificates without reopening the forcing chain (T5 J-uniqueness, T6 $\phi$). No downstream consumers are wired yet in the graph; the lemma stands as the module's public nonempty witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.