RSCosmo008Cert
plain-language theorem explainer
Certificate bundle for Cosmology Module 8 (reionization): the domain cost vanishes on the diagonal, stays non-negative for positive mass/energy arguments, and the canonical threshold is strictly positive. Cosmology auditors cite it as the structural witness that the module's cost and threshold axioms are inhabited. The declaration is a pure structure packing three Prop fields; inhabitation is supplied downstream by `cert`.
Claim. A certificate consists of three facts: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 8 sits in the RS cosmology stack and targets reionization. The module doc states the structural claim: the phi-ladder window $\phi^4$ to $\phi^5$ (numerically about $6.85$–$11.09$) matches the observed reionization redshift band $z_{\mathrm{reion}}\sim 7$–$10$, with status STRUCTURAL THEOREM (zero sorry, zero axiom).
The local cost is a two-argument real function domainCost used as the module's recognition cost on mass/energy-like coordinates. Its diagonal vanishing and nonnegativity mirror the global J-cost calculus: upstream, cost_nonneg records that every recognition event has nonnegative cost via Cost.Jcost_nonneg on a positive state. The third field is positivity of canonicalThreshold, the cutoff that marks the reionization window on the phi ladder.
Together these three propositions are the interface a later witness must satisfy before the module can claim a certified cost/threshold package.
proof idea
No proof body: this is a structure definition whose fields are propositions. Inhabitation is not proved here. Downstream, the noncomputable definition cert fills the three fields by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The theorem cert_inhabited then packages ⟨cert⟩ as Nonempty RSCosmo008Cert. The only upstream content used conceptually is the global nonnegativity of recognition cost (cost_nonneg / J-cost minimum at identity).
why it matters
This structure is the typed contract for RS Cosmology Module 8. Downstream cert and cert_inhabited discharge it, turning the reionization module into an inhabited structural certificate rather than a loose collection of lemmas. In the broader framework it anchors the reionization MATCH claim (phi-ladder band $\phi^4$–$\phi^5$ against $z_{\mathrm{reion}}\sim 7$–$10$) to the same cost nonnegativity and threshold positivity pattern used elsewhere in the forcing and observer layers. It does not itself compute redshifts or close the full cosmological forcing chain (T0–T8); it only standardizes the cost/threshold interface those numerical and structural claims sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.