cert_inhabited
plain-language theorem explainer
The certificate bundle for Cosmology Module 9 is nonempty: there exists a record packing the domain-cost identities and the positive canonical threshold used in the baryon-density structural claim. Cosmologists citing the RS structural match J(φ)(1−J(φ))/2 ≈ Ω_b use this inhabitation to discharge Nonempty obligations. The proof is a one-line term that exhibits the packaged cert instance.
Claim. There exists a certificate packing three facts: the domain cost vanishes on the diagonal ($C(r,r)=0$ for $r\neq 0$), the domain cost is nonnegative for positive arguments, and the canonical threshold is strictly positive.
background
Module 9 is the structural cosmology claim that the baryon density parameter arises from the J-cost at the golden ratio: $J(\varphi)(1-J(\varphi))/2 \approx 0.052$, compared with the observed $\Omega_b \approx 0.0493$. Status is structural (zero sorry, zero axiom).
The certificate structure packages three elementary properties of the module's domain cost $C$ and its canonical threshold $T$: diagonal vanishing $C(r,r)=0$ for $r\neq 0$, nonnegativity $C(m,e)\ge 0$ whenever $m,e>0$, and $T>0$. Domain cost is the local cost functional imported from the Cost layer; the threshold is the positive scale against which the structural density expression is read.
J itself is the unique cost forced by the Recognition Composition Law (T5): $J(x)=(x+x^{-1})/2-1$. The module sits downstream of Constants and Cost, not of the full forcing chain T0–T8.
proof idea
One-line term proof. The structure is inhabited by the already-constructed value cert, so Nonempty is witnessed by the anonymous constructor ⟨cert⟩. No tactics, no further lemmas.
why it matters
Closes the inhabitation obligation for the Module 9 certificate so downstream cosmology code can assume a concrete pack of cost identities rather than re-prove diagonal vanishing, nonnegativity, and threshold positivity. The parent scientific claim is the structural baryon-density match $J(\varphi)(1-J(\varphi))/2\sim\Omega_b$; this theorem does not restate that numerical comparison, only that the supporting certificate type is lived-in.
No used-by edges are recorded yet; the declaration is the terminal inhabitation step inside the module. It touches no open scaffold: the module is already marked structural with zero sorry. Framework landmarks in play are the J-cost (T5) and $\varphi$ as the self-similar fixed point (T6), which fix the numerical value being compared to $\Omega_b$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.