NuclearShellGapRS
plain-language theorem explainer
Interface packing three cost and threshold axioms for the RS nuclear shell-gap certificate: diagonal vanishing of domain cost, nonnegativity for positive arguments, and a strictly positive canonical threshold. Nuclear and cost-layer workers cite it when inhabiting the shell-gap certificate. Pure structure definition; no proof body, discharged by the sibling certificate construction.
Claim. A nuclear shell-gap certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost at $(r,r)$ vanishes; (ii) for all positive mass and energy arguments $m,e>0$, the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats the nuclear shell gap near magic number 50 (empirically about 3–5 MeV) in Recognition Science units. The local claim is a structural match: $\varphi^3,\mathrm{MeV}\approx 4.24,\mathrm{MeV}$ lies in that band, so the gap is read as a positive rung on the $\varphi$-ladder rather than a free nuclear parameter.
Domain cost is the local cost functional on mass/energy-like reals (imported from the Cost layer and Constants). The first field requires exact cancellation on the diagonal $m=e\neq 0$. The second requires nonnegativity off that diagonal for positive arguments, in the same spirit as the foundation fact that every recognition-event cost is nonnegative. The third field only asks that the module’s canonical threshold be positive, so the gap scale is a genuine barrier rather than a zero or sign flip.
Status in the module header is structural theorem (zero sorry, zero axiom): the physics match is packaged as inhabitability of this interface, not as a floating numerical assertion.
proof idea
No proof body: this is a structure declaration whose three fields are propositions. Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Those lemmas in turn rest on the Cost-layer nonnegativity pattern (cf. foundation cost_nonneg: recognition-event cost is nonnegative via Jcost_nonneg). The structure itself only names the interface.
why it matters
Gives the typed certificate that the nuclear shell-gap module must inhabit. Downstream, cert builds a concrete value of this structure, and cert_inhabited records Nonempty NuclearShellGapRS, closing the module’s structural claim.
In the broader RS picture this is a domain-level application of the cost calculus (J-cost nonnegativity and diagonal minimum) to nuclear phenomenology: the shell gap at magic 50 is identified with a positive $\varphi$-ladder scale ($\varphi^3$ MeV in band), not an independent fit parameter. It does not touch the T0–T8 forcing chain directly; it sits in the nuclear application layer that consumes Constants and Cost after those foundations are fixed.
Open content is interpretive rather than formal: whether $\varphi^3$ MeV is the unique or preferred identification among nearby ladder rungs remains a physics reading, while the Lean side only certifies cost axioms plus threshold positivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.