cert
plain-language theorem explainer
Packages three elementary properties of the domain J-cost (vanishing on the diagonal, nonnegativity for positive arguments, and a strictly positive canonical threshold) into a single certificate structure for the exact BBN He-4 match. Cosmologists checking the RS helium abundance claim cite this bundle. The body is a pure structure constructor wiring three already-proved sibling lemmas.
Claim. There is 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. Together these certify the structural side of the exact primordial $^4\mathrm{He}$ mass-fraction match from $J$-cost.
background
The module treats primordial helium-4 abundance as a structural consequence of the Recognition Science $J$-cost. Measured $Y_p\approx 0.2454$ is matched by the RS formula $Y_p=J(\varphi)\cdot 2.08\approx 0.118\cdot 2.08=0.245$, equivalently $J(\varphi)\cdot 2\cdot\varphi^{0.6}$. Status is a structural theorem with zero sorry and zero axioms.
domainCost is the local cost functional on mass/energy pairs used for the BBN comparison; the certificate structure BBNHeliiumExact3Cert packages the three properties needed before any numerical threshold comparison: diagonal vanishing, nonnegativity, and a positive threshold. Upstream, cost_nonneg from ObserverForcing records that every recognition event has nonnegative $J$-cost via Jcost_nonneg at positive state.
proof idea
Pure structure construction. The three fields of BBNHeliiumExact3Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional tactics or algebraic work; the def is a one-shot witness assembly.
why it matters
Gives a named, reusable certificate that the domain $J$-cost is a legitimate nonnegative cost with a positive comparison threshold, which is the structural prerequisite for claiming an exact BBN He-4 match from $J(\varphi)$. The module frames this as the final-session exact version of the primordial helium prediction. No downstream consumers are recorded yet; the natural parent is any theorem that consumes BBNHeliiumExact3Cert to discharge the numerical $Y_p$ identity. Ties to the RS forcing chain only indirectly through the $J$-cost (T5 uniqueness) and $\varphi$ (T6 fixed point) that underlie the abundance formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.