cert
plain-language theorem explainer
Packages three nuclear domain-cost facts into a single Bethe–Weizsäcker certificate: diagonal vanishing, non-negativity for positive mass/energy, and a positive canonical threshold. Anyone wiring RS nuclear binding to the cost layer cites this witness. The body is a pure structure assembly from three sibling lemmas.
Claim. There is a certificate asserting: (i) the nuclear domain cost vanishes on the diagonal, $\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
This module is the RS nuclear layer (session 3), status structural with zero sorry and zero axioms. The classical Bethe–Weizsäcker semi-empirical mass formula writes binding energy as volume, surface, Coulomb, and asymmetry terms in $A$ and $Z$. RS aims to pin the coefficients to the recognition cost $J$ and the coherence energy $E_{\mathrm{coh}}$, with $\phi$-ladder scalings noted in the module header.
The certificate structure collects three cost-layer obligations on domainCost: equality to zero when the two arguments match (away from zero), non-negativity for positive mass and energy parameters, and positivity of a fixed canonical threshold. Upstream, recognition-event cost is already known non-negative via $J$-cost non-negativity on positive states; the nuclear domain cost is the local specialization of that idea.
proof idea
One-line structure construction. The three fields of the certificate are filled by the sibling facts domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No extra algebra or case analysis appears in the body.
why it matters
Gives a single named witness that the nuclear cost interface meets the three structural axioms expected by a Bethe–Weizsäcker-style RS binding model. Downstream consumers (none wired yet in the graph) can take this certificate rather than re-proving diagonal vanishing, non-negativity, and threshold positivity. It sits under the broader RS program of deriving nuclear scales from $J$ and the $\phi$-ladder (module notes compare volume coefficient candidates such as $J(\phi)^{-1}E_{\mathrm{coh}}$ against the empirical $\sim 15.8,\mathrm{MeV}$). Does not yet close the coefficient-matching problem flagged in the module doc; it only certifies the cost-side interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.