cert
plain-language theorem explainer
Packages three domain-cost facts into a single matter-radiation equality certificate: cost vanishes on the diagonal, is nonnegative for positive densities, and the canonical threshold is positive. Cosmology auditors cite it when wiring RS equality redshift into larger certificate stacks. The body is pure structure packing of three already-proved sibling lemmas.
Claim. There exists a certificate asserting: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is 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 matter-radiation equality redshift in Recognition Science units. Observationally $z_{\mathrm{eq}}\sim 3400$; the RS match is $z_{\mathrm{eq}}=\varphi^{17}\cdot 0.95\approx 3392$, using the golden-ratio ladder forced by the T5-T6 uniqueness of the J-cost $J(x)=(x+x^{-1})/2-1$ and its self-similar fixed point $\varphi$.
domainCost is the local cost functional on a pair of positive scale factors (matter vs radiation densities in RS-native units). The certificate structure MatterRadEqCert records the three algebraic properties needed before any numerical threshold comparison: vanishing on the equal-density diagonal, nonnegativity off-diagonal, and positivity of the canonical threshold.
Upstream, nonnegativity of recognition cost is the standard J-cost fact (cost_nonneg: every recognition event has nonnegative cost because $J\ge 0$ for positive arguments).
proof idea
One-line structure inhabitant. The three fields of MatterRadEqCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No new algebra is performed; the definition only bundles those proofs into a single certificate value.
why it matters
Gives the module a named, zero-sorry certificate object for matter-radiation equality, matching the module status line "STRUCTURAL THEOREM (0 sorry, 0 axiom)". In the RS cosmology stack this is the local well-posedness token before comparing the equality redshift to the $\varphi$-ladder value $\varphi^{17}\cdot 0.95\approx 3400$.
No downstream consumers appear in the current graph (used_by empty), so the immediate role is documentary and compositional: later equality or redshift theorems can take MatterRadEqCert as a hypothesis rather than re-proving diagonal vanishing and threshold positivity. It sits downstream of the forcing-chain cost nonnegativity (T5 J-uniqueness lineage) and upstream of any numerical $z_{\mathrm{eq}}$ match claims in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.