cert_inhabited
plain-language theorem explainer
The certificate bundle for RS cosmology module 6 is inhabited: there exists a package of the domain-cost diagonal identity, nonnegativity, and positive canonical threshold. Cosmology auditors and anyone wiring the DM-mass structural layer cite this. The proof is a one-line term witness from the concrete certificate instance.
Claim. The type of certificates for RS cosmology module 6 is nonempty. Such a certificate packages three facts: the domain cost vanishes on the diagonal ($C(r,r)=0$ for $r\neq 0$), the domain cost is nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive.
background
Module 6 of the RS cosmology stack is a structural layer tied to a dark-matter mass claim $M_W/45 = 1.787,\mathrm{GeV}$, flagged as testable against the XENONnT program (2026). The module status is a structural theorem: zero sorry, zero axioms.
The certificate structure packages three elementary properties of the local domain cost and threshold. Domain cost is the cost functional restricted to this cosmology domain (imported from the Cost layer and Constants). The diagonal identity says cost of matching a scale to itself is zero; nonnegativity is the usual cost lower bound for positive mass and energy; the canonical threshold is required to be strictly positive so the module's cutoff is well-defined.
Upstream, the structure itself is the only dependency: inhabitation means a concrete record of those three propositions exists in the module.
proof idea
Term-mode one-liner. The module already defines a concrete certificate value cert of type RSCosmo006Cert. The proof is the standard Nonempty introduction: the anonymous constructor ⟨cert⟩ supplies that value as a witness. No tactics, no further lemmas.
why it matters
In the Recognition cosmology stack this is the inhabitation seal for module 6's structural certificate. Downstream consumers (none listed yet in the graph) can assume a nonempty certificate type rather than threading the three fields by hand. The module doc ties the layer to a concrete DM mass figure and an external falsifier window (XENONnT 2026), so the certificate is the Lean-side guarantee that the cost and threshold scaffolding is coherent before any observational comparison. It does not itself derive the mass number from the forcing chain (T0–T8) or from the Recognition Composition Law; it only certifies the local cost/threshold package used by that TESTABLE claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.