cert
plain-language theorem explainer
Packages three elementary cost facts into a reionization certificate: diagonal vanishing, nonnegativity for positive mass/energy, and a positive canonical threshold. Cosmologists matching RS phi-ladder brackets to z_reion cite this bundle. The body is a structure instance that wires three local lemmas; no new algebra.
Claim. There is a reionization certificate asserting: (i) the domain cost of any nonzero ratio against itself is zero; (ii) for positive mass and energy parameters the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats the cosmic reionization redshift $z_{\mathrm{reion}}\sim 7$–$10$ in Recognition Science units. The golden ratio powers $\varphi^4\approx 6.85$ and $\varphi^5\approx 11.09$ bracket the observed window, so the claim is structural consistency rather than a new fit.
Domain cost is the local J-cost comparison used for the epoch threshold: it vanishes when the two arguments coincide (away from zero) and stays nonnegative on the positive quadrant. The canonical threshold is the positive cutoff against which that cost is read. Upstream, the same certificate shape appears in the astrophysics J-cost reionization epoch module; the foundation lemma that every recognition-event cost is nonnegative (via $J\ge 0$) supplies the sign pattern this module reuses.
proof idea
One-line structure instance. The three fields of ReionizationCert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity on positives), and canonicalThreshold_pos (strict positivity of the threshold). No tactics beyond field assignment.
why it matters
Gives an inhabited certificate that the cost/threshold side of the RS reionization-redshift story is well-formed, matching the module claim that $\varphi^4$–$\varphi^5$ brackets $z_{\mathrm{reion}}$. It sits beside the parallel certificate shapes in Astrophysics.ReionizationEpochFromJCost and Cosmology.ReionizationHistoryFromRS (the latter tracks five epochs with successive boundary redshifts in exact $\varphi$ ratio). In the forcing chain this is downstream of T5 J-uniqueness and T6 $\varphi$ as self-similar fixed point; the numerical window also touches $Z_{\mathrm{cf}}=\varphi^5\in(11,12)$. No downstream consumers are wired yet; the object is the local closure of the cost axioms for this cosmology page.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.