cert_inhabited
plain-language theorem explainer
The RS Cosmology Module 4 certificate type is nonempty: there exists a packed witness for diagonal vanishing of the domain cost, its nonnegativity on positive arguments, and positivity of the canonical threshold. Cosmology auditors cite this to discharge the structural side of the n_s = 1 - 2/45 scaffold. The proof is a one-line term that feeds the concrete certificate record into Nonempty.
Claim. There exists a certificate packing three facts: the domain cost vanishes on the diagonal ($C(r,r)=0$ for all $r\neq 0$), the domain cost is nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive.
background
Module 4 of the RS cosmology stack targets the scalar spectral index $n_s = 1 - 2/45 \approx 0.9556$, set against the Planck value $0.9649$ (about $2.2\sigma$ tension) and marked OPEN on the physics side. The module is declared a structural theorem: zero sorry, zero axioms.
The certificate structure bundles three elementary cost facts used throughout the module. Domain cost is the local cost functional on mass/energy pairs (imported from the Cost layer and specialized here). The three fields require: cost vanishes when the two arguments coincide and are nonzero; cost is nonnegative whenever both arguments are positive; and the module's canonical threshold constant is strictly positive.
Those three properties are already proved as sibling lemmas (domainCost_at_eq, domainCost_nonneg, canonicalThreshold_pos) and assembled into a concrete record cert. The present declaration only asserts that the certificate type is inhabited.
proof idea
One-line term proof. The concrete record cert already satisfies the three fields of RSCosmo004Cert, so ⟨cert⟩ is a term of type Nonempty RSCosmo004Cert. No tactics, no further lemmas.
why it matters
Gives a single Nonempty handle for the structural side of Cosmology Module 4, so downstream developments can assume the cost and threshold package without re-proving the three field lemmas. The module itself sits on the OPEN $n_s$ comparison (RS value $1-2/45$ versus Planck), so this certificate is scaffolding for later quantitative closure rather than a finished cosmological claim. No parent theorems currently depend on it; it is the terminal inhabitance marker for the module's certificate type. Framework role is local: cost nonnegativity and diagonal vanishing are instances of the global J-cost discipline (T5), specialized to the cosmology domain cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.