cert
plain-language theorem explainer
Packages three nuclear-domain cost facts into a single certificate: the domain cost vanishes on the diagonal, is nonnegative for positive mass and energy, and the canonical threshold is positive. Nuclear-structure work that needs a ready-to-hand witness of these J-cost properties cites this bundle. The body is a pure structure constructor wiring three already-proved sibling lemmas.
Claim. There is a certificate recording that (i) for every nonzero real $r$, the nuclear domain cost satisfies $\mathrm{domainCost}(r,r)=0$; (ii) for all positive reals $m,e$, $\mathrm{domainCost}(m,e)\ge 0$; and (iii) the canonical threshold is strictly positive.
background
The module develops a structural account of nuclear magic numbers from the Recognition Science phi-ladder (Plan v7 session 3). Empirically the closed shells sit at $2,8,20,28,50,82,126$. The RS ansatz writes $N_{\mathrm{magic},k}=\varphi^k\cdot 2$, producing the comparison sequence $2,5,9,14,22,36,58$ against the empirical list; the present file is marked structural (zero sorry, zero axiom).
The certificate structure NucMagicNumbers2Cert packages three domain-level cost axioms needed before any threshold comparison: vanishing of the cost on equal arguments, nonnegativity for positive mass and energy, and positivity of the canonical threshold. Domain cost is the nuclear specialization of the J-cost $J(x)=(x+x^{-1})/2-1$ from the forcing chain (T5). Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via Cost.Jcost_nonneg.
proof idea
One-line structure constructor. The three fields of NucMagicNumbers2Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional tactics or algebraic work occur at this site; the definition only assembles already-established facts into the certificate record.
why it matters
Gives a single named inhabitant of the nuclear magic-number certificate so downstream nuclear lemmas can assume the three cost properties by projecting fields rather than re-proving them. The module status line marks the whole development as a structural theorem with no sorry and no axiom, so this bundle is the concrete witness that the J-cost side conditions are discharged. It sits in the nuclear domain of the RS program, where magic numbers are read off the phi-ladder ($N_{\mathrm{magic},k}=\varphi^k\cdot 2$) rather than from shell-model phenomenology. No used-by edges are recorded yet; the natural consumers are threshold-comparison and shell-closure statements that need a ready certificate. Ties to the T5 J-uniqueness landmark via the underlying cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.