cert
plain-language theorem explainer
Packages the three elementary J-cost facts needed for the baryon-fraction certificate: diagonal cost vanishes, cost is nonnegative off the diagonal, and the canonical threshold is positive. Cosmologists citing the RS claim Ω_b/Ω_total = J(φ) ≈ 0.118 use this bundle as the structural witness. Construction is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There exists a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module derives a structural certificate for the RS baryon fraction claim: $\Omega_b/\Omega_{\mathrm{total}}=J(\varphi)\approx 0.118$, compared with the Planck 2018 ratio $\Omega_b/\Omega_m\approx 0.157$. Status is structural (zero sorry, zero axiom).
The cost is the Recognition Science J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by T5. Domain cost is the two-argument form used for mass/energy pairs in the cosmology layer. The canonical threshold is the positive cutoff against which the baryon-sector cost is compared.
Upstream, nonnegativity of recognition-event cost is already established in ObserverForcing via $J$-cost nonnegativity on positive states. The three field lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos are proved as siblings in this module.
proof idea
One-line structure instance. The three fields of OmegaBaryon3Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive mass/energy), and canonicalThreshold_pos (strict positivity of the threshold). No additional tactic work.
why it matters
This is the inhabiting certificate for the Plan v7 baryon-fraction structural theorem. It packages the minimal J-cost hygiene (vanishing on the identity ray, nonnegativity, positive threshold) required before any numerical comparison of $J(\varphi)$ with observed $\Omega_b/\Omega_m$ can be stated inside Lean.
It sits on the T5 J-uniqueness landmark and the RCL identity that forces $J$. The module itself notes the order-of-magnitude match ($J(\varphi)\approx 0.118$ vs Planck $\approx 0.157$) without claiming exact equality. No downstream consumers are recorded yet; the sibling cert_inhabited is the natural next witness that the type is nonempty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.