cert_inhabited
plain-language theorem explainer
The structural certificate for RS cosmology gap-45 is inhabited: a witness packs diagonal vanishing of domain cost, nonnegativity for positive arguments, and positivity of the canonical threshold. Cosmology auditors cite it to discharge Nonempty obligations when wiring the gap-45 package into rung or forcing arguments. The proof is a one-line term constructor from the packaged certificate value.
Claim. The type of structural certificates for RS cosmology gap-45 is nonempty: there exists a witness asserting that domain cost vanishes on the diagonal ($C(r,r)=0$ for all $r\neq 0$), is nonnegative for positive mass and energy arguments, and that the canonical threshold is strictly positive.
background
Module RS_COS_Structural_004 packages the structural side of RS gap-45. At spatial dimension $D=3$ one has $D^2(D+2)=9\cdot 5=45$, read as the minimum rung for stable self-reference on the $\varphi$-ladder. Status is a pure structural theorem (no sorry, no axioms).
The certificate structure bundles three facts about a real bivariate domain cost $C(m,e)$ and a fixed positive threshold $T$: (i) $C(r,r)=0$ whenever $r\neq 0$; (ii) $C(m,e)\ge 0$ for $m>0$, $e>0$; (iii) $T>0$. Domain cost is the local cost functional imported from the Cost layer (the same J-family that satisfies the Recognition Composition Law), specialized to mass/energy arguments in the cosmology setting.
Sibling lemmas already prove each field separately (diagonal identity, nonnegativity, threshold positivity). The certificate is their product type; this theorem only records that the product is inhabited.
proof idea
One-line term proof. The module already builds a concrete value cert : RSCOSStructural004Cert by packing the three sibling proofs. Nonemptiness is then the anonymous constructor ⟨cert⟩, i.e. the standard introduction rule for Nonempty. No further rewriting or case analysis.
why it matters
Gap-45 is the structural lower bound on rung for stable self-reference once $D=3$ is forced (forcing chain T8). This inhabitation lemma closes the certificate API for the module so downstream cosmology developments can assume a single Nonempty hypothesis rather than three separate field lemmas.
No used_by edges are recorded yet; the declaration is the terminal export of the structural package. In the broader RS ledger it sits beside the eight-tick octave (T7) and the $\varphi$-ladder mass formula: any argument that needs "the gap-45 cost package is available" cites this Nonempty fact. It does not itself compute particle masses or match observational $H_0$/BAO data; it only certifies the algebraic cost skeleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.