ReionEnd3Cert
plain-language theorem explainer
Certificate bundling three structural properties for the RS reionization-end claim: diagonal vanishing of domain cost, nonnegativity for positive mass/energy arguments, and positivity of the canonical threshold. Cosmology workers matching z_end to the phi ladder cite this as the interface type. Pure structure definition; no proof body.
Claim. A reionization-end certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost at $(r,r)$ equals zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats the end of cosmic reionization as a J-cost endpoint. Observationally $z_{\mathrm{end}}\sim 5.5$–$6$ (Planck); RS places the same scale on the golden-ratio ladder, with $\phi^3\approx 4.24$ and $\phi^4\approx 6.85$, so $z_{\mathrm{end}}=\phi^4$ is the working identification.
Domain cost is the local cost functional on a pair of positive reals (mass- and energy-like arguments), built from the RS J-cost $J(x)=(x+x^{-1})/2-1$. The diagonal identity $J(1)=0$ forces vanishing when the two arguments coincide. Nonnegativity of recognition cost is the upstream fact from ObserverForcing: every recognition event has cost $\ge 0$, via Jcost_nonneg.
The canonical threshold is the positive cutoff that marks completion of reionization in these units. The certificate simply packages the three algebraic properties the endpoint argument needs.
proof idea
No proof: this is a structure declaration. It names three fields (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold) and stops. Inhabitation is deferred to the sibling cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives the typed interface for the structural reionization-end theorem in this module (status: 0 sorry, 0 axiom). Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty of the certificate type, so later cosmology lemmas can assume the three properties without re-proving them.
In the RS forcing picture the endpoint sits on the phi ladder near $\phi^4$, consistent with Planck $z_{\mathrm{end}}\sim 5.5$–$6$. The certificate isolates the pure cost-algebra ingredients (J-minimum on the diagonal, cost nonnegativity, positive threshold) from the numerical redshift identification, keeping the structural layer clean for the Plan v7 pass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.