cert
plain-language theorem explainer
Certificate that the nuclear shell-gap cost structure is inhabited: the domain cost vanishes on equal arguments, is nonnegative for positive inputs, and the canonical threshold is strictly positive. Cited by anyone packaging the RS claim that φ³ MeV sits in the magic-50 shell-gap band. The body is a structure instance wiring three local lemmas; no new algebra.
Claim. There exists a witness that the nuclear shell-gap domain cost $C$ satisfies: (i) $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
The module packages a Recognition Science reading of the nuclear shell gap near magic number 50 (empirically ~3–5 MeV). In RS units the candidate scale is $\varphi^3\approx 4.236$, which lands inside that band; the module status line calls this a structural theorem with no sorry and no axioms.
NuclearShellGapRS is the local certificate structure. It demands three properties of a domain cost $C$ and a canonical threshold $T$: diagonal vanishing ($C(r,r)=0$), nonnegativity on the positive quadrant, and $T>0$. The domain cost is the nuclear specialization of the RS J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$).
Upstream, nonnegativity of recognition cost is already known from ObserverForcing: "The cost of any recognition event is non-negative," via Jcost_nonneg at positive state. The three field fillers domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos are in-module siblings that discharge the structure fields for this nuclear specialization.
proof idea
One-line structure instance. The three fields of NuclearShellGapRS are filled by the preexisting local lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity on positive mass/energy), and canonicalThreshold_pos (strict positivity of the canonical threshold). No tactics and no new calculation; pure witness assembly.
why it matters
Gives a single named inhabitant of the nuclear shell-gap certificate structure, so downstream nuclear claims can assume the cost axioms by projecting fields off this witness rather than re-proving them. The module doc ties the construction to the RS match $\varphi^3,\mathrm{MeV}\sim 4.24$ against the empirical 3–5 MeV gap at magic number 50.
In the broader forcing chain this sits downstream of T5 J-uniqueness (the cost shape) and the phi fixed point (T6), specialized to nuclear scales. No used_by edges are recorded yet; the natural consumer is any theorem that needs a packaged proof that the nuclear domain cost is a genuine RS cost with positive threshold. Sibling cert_inhabited likely records mere existence from this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.