ReionizationCert
plain-language theorem explainer
Certificate record for the RS reionization-redshift claim: domain cost vanishes on the diagonal, is non-negative for positive arguments, and the canonical threshold is positive. Cosmology and astrophysics modules inhabit it to lock the structural side of the z_reion ~ phi^4..phi^5 bracket. Pure structure definition; no proof body.
Claim. A reionization certificate is a triple of assertions: the domain cost satisfies $C(r,r)=0$ for all $r\neq 0$; $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; and the canonical threshold $T$ obeys $T>0$.
background
The module treats cosmic reionization redshift in Recognition Science units. Observed $z_{\mathrm{reion}}$ lies roughly in $7$--$10$. The golden ratio powers $\varphi^4\approx 6.85$ and $\varphi^5\approx 11.09$ bracket that window, so the structural claim is that the RS cost geometry places the reionization threshold inside $[\varphi^4,\varphi^5]$.
Domain cost is the local cost functional on mass/energy (or scale) pairs used in this cosmology layer; it inherits non-negativity from the underlying $J$-cost ($J(x)=(x+x^{-1})/2-1$), whose non-negativity is already forced upstream (cost_nonneg on recognition events). The canonical threshold is the positive scale against which that cost is compared when marking the reionization boundary.
Sibling lemmas in the same file establish diagonal vanishing, non-negativity, and threshold positivity; this structure simply packages those three props as a single certificate type.
proof idea
No proof: this is a structure declaration. Its three fields are propositional hypotheses (diagonal vanishing of domain cost, non-negativity for positive arguments, positivity of the canonical threshold). Downstream cert fills the fields by pointing at the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a uniform certificate type for the structural half of the RS reionization story. Same-module cert and cert_inhabited inhabit it; the astrophysics twin ReionizationEpochFromJCost reuses the identical field shape, while ReionizationHistoryFromRS carries a parallel certificate (five epochs, successive boundary redshifts in exact ratio $\varphi$, all boundaries positive). Together they support the module claim that $\varphi^4$--$\varphi^5$ brackets $z_{\mathrm{reion}}$, tying the cosmology layer to the forced $\varphi$ fixed point (T6) and the non-negative $J$-cost geometry without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.