cert
plain-language theorem explainer
Packages the three elementary J-cost facts needed for the reionization-end certificate: diagonal cost vanishes, cost is nonnegative off the axes, and the canonical threshold is positive. Cosmologists citing the RS z_end ~ phi^4 prediction use this bundle as the structural witness. Construction is a pure structure inhabitant wiring three already-proved lemmas.
Claim. There exists a certificate recording that the domain cost $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical reionization threshold $T$ satisfies $T>0$.
background
The module treats the end of cosmic reionization as a J-cost threshold crossing. Recognition Science places $z_{\mathrm{end}}$ on the phi ladder near $\phi^4\approx 6.85$, consistent with Planck's $z_{\mathrm{end}}\sim 5.5$--$6$. The local cost is the standard RS J-cost pulled back to a two-argument domain cost on positive reals.
ReionEnd3Cert is the structure that packages the three elementary properties any such endpoint argument needs: vanishing on the diagonal (identity events cost nothing), nonnegativity for positive mass and energy arguments, and positivity of the canonical threshold. Upstream, nonnegativity of recognition cost is the global fact that $J\ge 0$ with minimum at the identity ratio $x=1$.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further tactic work.
why it matters
Gives a single named witness that the J-cost side conditions for the reionization-end structural theorem are discharged. The module is marked structural (0 sorry, 0 axiom) and sits in the cosmology layer that ties the phi-ladder mass/redshift formula to observational endpoints. With no further downstream edges yet, this certificate is the reusable handle for any later theorem that needs the three cost axioms in one place. It does not itself compute $z_{\mathrm{end}}$; it only certifies the cost infrastructure used by that claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.