cert_inhabited
plain-language theorem explainer
The reionization certificate bundle is nonempty: there is a concrete witness packing diagonal vanishing of the domain cost, its nonnegativity on positive arguments, and positivity of the canonical threshold. Cosmologists citing the RS Module 8 structural match (phi^4–phi^5 to z_reion ~7–10) use this as the existence hook. Proof is a one-line term that inhabits Nonempty from the packaged cert value.
Claim. The type of reionization certificates is inhabited: there exists a record whose fields assert (i) the domain cost vanishes on the diagonal, $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; and (iii) the canonical threshold is strictly positive.
background
Module 8 of the RS cosmology stack treats reionization as a structural match: the interval from $\varphi^4$ to $\varphi^5$ (numerically about 6.85–11.09) is identified with the observed reionization redshift window $z_{\mathrm{reion}}\sim 7$–$10$. The module is marked as a structural theorem with no sorrys and no axioms.
The certificate structure packages three elementary properties of the local domain cost $C$ and the canonical threshold $T_$: diagonal vanishing $C(r,r)=0$ off zero, nonnegativity for positive mass and energy arguments, and $T_>0$. These are the minimal algebraic facts needed before any redshift-band comparison is stated.
Upstream, the structure itself is the sole dependency; the inhabiting value cert is the sibling that already assembles the three field proofs.
proof idea
Term-mode one-liner. Nonemptiness of the certificate type is witnessed by the already-constructed value cert, introduced via the anonymous constructor ⟨cert⟩. No tactics, no further lemmas: the proof is pure inhabitation of Nonempty from a concrete package of the three field obligations.
why it matters
Gives a single named existence fact for the Module 8 certificate so downstream cosmology text can cite “the reionization cert is inhabited” rather than re-proving diagonal vanishing, nonnegativity, and threshold positivity. The module doc frames the scientific claim as the $\varphi^4$–$\varphi^5$ band matching $z_{\mathrm{reion}}\sim 7$–$10$; this theorem is the Lean-side existence gate for that structural package.
No downstream users are recorded yet, so the declaration presently closes the module’s certificate API rather than feeding a larger forcing-chain step. It sits in the cosmology layer, not in T0–T8, but inherits the global $\varphi$-ladder numerics ($\varphi^4$, $\varphi^5$) that the primer associates with RS-native scales. Open questions about detailed reionization microphysics are out of scope; the cert only locks the cost/threshold skeleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.