RSCosmo007Cert
plain-language theorem explainer
Certificate bundle for Cosmology Module 7 (matter-radiation equality near z_eq ~ 3400). It packages three structural facts: the domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cosmology and RS-forcing readers cite it as the typed witness that the module's cost/threshold interface is inhabited. The structure itself is pure data; inhabitants are assembled from sibling lemmas.
Claim. A certificate consists of three properties of the module's domain cost $C$ and canonical threshold $\tau$: (i) $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
Module 7 targets matter-radiation equality in the RS cosmology stack: the claimed match is $\phi^{17}\cdot 0.95\approx z_{\mathrm{eq}}\sim 3400$ against the empirical $z_{\mathrm{eq}}\approx 3400$, recorded as a structural theorem (zero sorry, zero axiom).
The domain cost $C(m,e)$ is the local comparison cost between two positive real scales (matter-like and energy-like). Its diagonal vanishing and nonnegativity mirror the global J-cost calculus: upstream, cost_nonneg states that every recognition event has nonnegative cost, via $J$-cost nonnegativity on positive states. The canonical threshold $\tau$ is the positive cutoff used by the module's equality test.
The certificate is the Prop-level interface those three facts must satisfy before the module exports an inhabited witness.
proof idea
No proof body: this is a structure declaration. It only names the three fields (diagonal vanishing of domain cost, nonnegativity of domain cost on the positive quadrant, positivity of the canonical threshold). Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to the nonempty theorem that wraps that witness.
why it matters
Gives Module 7 a single typed certificate rather than three loose lemmas, so downstream code can demand one object. Immediate consumers are the canonical inhabitant and the Nonempty theorem in the same module; together they close the structural side of the matter-radiation equality claim ($\phi^{17}\cdot 0.95\sim 3400$).
In the broader RS stack this sits under cosmology forcing that already uses the J-cost minimum and nonnegativity (T5 J-uniqueness lineage, RCL). It does not itself derive $z_{\mathrm{eq}}$ from the forcing chain; it only certifies the cost/threshold interface the equality match relies on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.