cert_inhabited
plain-language theorem explainer
The cosmology structural certificate for module 9 is inhabited: a single witness packs diagonal vanishing and nonnegativity of the domain cost together with positivity of the canonical threshold. Auditors of the RS cosmology layer cite it to discharge Nonempty goals when wiring this module into larger structural arguments. The proof is a one-line term that exhibits the prebuilt certificate value.
Claim. The type of structural certificates for cosmology module 9 is nonempty: there exists a record packing (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) strict positivity of the canonical threshold.
background
Module RS_COS_Structural_009 sits in the cosmology layer of the Recognition Science forcing chain (T5 J-uniqueness through T8 forcing $D=3$). It is marked as a structural theorem block: zero sorry, zero axioms.
The certificate structure packages three elementary properties of a real bivariate domain cost and a positive real threshold. The first field asserts that the cost vanishes on the diagonal away from zero. The second asserts nonnegativity for strictly positive mass and energy arguments. The third asserts that the module's canonical threshold is positive. These are the only hypotheses the certificate carries; no dynamical or observational content is included.
Upstream, the structure itself is the sole dependency. Sibling lemmas in the same file establish the three fields pointwise (diagonal identity, nonnegativity, threshold positivity) and assemble them into a concrete certificate value.
proof idea
Term-mode one-liner. The proof is the anonymous constructor ⟨cert⟩, which inhabits Nonempty by exhibiting the already-assembled certificate value whose three fields have been proved by the sibling lemmas in this module. No further rewriting or case analysis occurs.
why it matters
In the RS cosmology stack, structural modules export inhabited certificate types so downstream forcing-chain and consistency arguments can assume the local cost and threshold facts without re-proving them. This declaration closes that export for module 9: once Nonempty is known, any consumer can obtain a concrete record and project the three packed properties.
The module doc places the work on the T5–T8 spine (J-uniqueness, $\varphi$ forced, eight-tick octave, $D=3$). The certificate itself is purely algebraic (cost diagonal, cost sign, threshold sign) and does not yet encode expansion history or observational constraints; it is the structural scaffold those later claims sit on. No downstream consumers are wired in the current graph, so the immediate role is local completeness of the module's export surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.