cert
plain-language theorem explainer
Packages a three-field certificate for the RS cosmology module on matter-radiation equality: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Cosmologists citing the structural z_eq match (phi^17 * 0.95 ~ 3400) use this as the inhabited witness. The body is a pure structure assembly from three sibling lemmas.
Claim. There exists a certificate asserting: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_Cosmo_007 treats matter-radiation equality in Recognition Science units. The headline numerical claim is $\phi^{17}\cdot 0.95 = z_{\mathrm{eq}}\sim 3400$, matching the empirical redshift of equality; the module is marked a structural theorem (zero sorry, zero axiom).
The local cost is a two-argument domain cost on positive reals (matter and radiation scale factors or densities). It is built from the RS J-cost $J(x)=(x+x^{-1})/2-1$, which is nonnegative and vanishes only at the identity $x=1$. Upstream, ObserverForcing records that every recognition-event cost is nonnegative via $J$-cost nonnegativity.
The certificate structure bundles three elementary properties needed before any threshold comparison: diagonal vanishing, off-diagonal nonnegativity, and positivity of the module's canonical threshold.
proof idea
One-line structure inhabitant. Each field is filled by a named sibling lemma already proved in the same module: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg (itself resting on the foundation fact that J-cost is nonnegative), and threshold positivity by canonicalThreshold_pos. No extra tactics or rewriting.
why it matters
Gives the inhabited certificate object for Cosmology Module 7, the structural theorem that pins matter-radiation equality at $z_{\mathrm{eq}}\sim 3400$ via $\phi^{17}\cdot 0.95$. In the RS ladder, powers of $\phi$ set cosmological scales; this module is one of the discrete redshift anchors. No downstream consumers are wired yet in the graph, so the certificate is presently a self-contained witness that the cost and threshold side-conditions hold. It closes the local scaffolding for the MATCH claim without introducing axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.