cert
plain-language theorem explainer
Packages the reionization-module certificate: domain cost vanishes on the diagonal, stays non-negative for positive arguments, and the canonical threshold is strictly positive. Cosmologists citing the RS Module 8 structural match (phi^4–phi^5 band to z_reion ~ 7–10) use this witness. The definition is a pure structure assembly of three sibling lemmas.
Claim. There is a reionization certificate consisting of three facts: for every nonzero real $r$, the domain cost of $(r,r)$ is zero; for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
Module 8 of the RS cosmology stack treats reionization as a structural match: the interval from $\phi^4$ to $\phi^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 (no sorry, no axioms).
The certificate type collects three elementary properties of the local domain cost. Domain cost is the recognition cost specialized to this cosmology module; it inherits non-negativity from the global J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$). The diagonal vanishing condition says that when model and evidence coincide the cost is zero. The canonical threshold is the positive scale against which the reionization band is compared.
Upstream, the foundation lemma that any recognition event has nonnegative cost supplies the pattern that the local non-negativity proof follows.
proof idea
One-line structure inhabitant. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra reasoning is performed at this site.
why it matters
Gives a single named witness that Module 8’s cost and threshold infrastructure is well-formed, so downstream cosmology code can assume diagonal vanishing, non-negativity, and a positive threshold without re-proving them. It sits inside the structural claim that the $\phi^4$–$\phi^5$ rung band matches the observed reionization window. In the broader forcing chain this is applied physics after T5 (J-uniqueness) and T6 ($\phi$ as self-similar fixed point): the cost is the forced J-cost, and the band edges are pure powers of $\phi$. No parent theorems currently depend on this certificate (used_by is empty); it is the module’s exportable proof object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.