cert
plain-language theorem explainer
Packages three nuclear-domain cost facts into a single NuclearShell3Cert value: diagonal vanishing of the domain cost, nonnegativity for positive mass and energy, and positivity of the canonical threshold. Anyone assembling the J-cost nuclear-shell certificate cites this bundle. The body is pure field assignment from three sibling lemmas already proved in-module.
Claim. There exists a nuclear-shell 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.
background
The module builds a structural link from the Recognition Science J-cost to the nuclear shell model's five canonical single-particle orbital families ($s_{1/2}$, $p_{1/2}$, $p_{3/2}$, $d_{3/2}$, $d_{5/2}$), identified with $\mathrm{configDim},D=5$. Status is a closed structural theorem (no sorry, no axioms).
The certificate structure NuclearShell3Cert records three elementary cost properties of the nuclear domain cost: it vanishes on the equal-argument diagonal (away from zero), stays nonnegative for positive mass and energy arguments, and the associated canonical threshold is positive. Upstream, nonnegativity of recognition cost is the standard J-cost fact that every recognition event has cost $\ge 0$ (via $J$-cost nonnegativity on positive states).
Sibling lemmas in the same file discharge each field: diagonal identity, domain-cost nonnegativity, and threshold positivity.
proof idea
One-line structure inhabitant. The three fields of NuclearShell3Cert are filled by direct assignment: diagonal vanishing from domainCost_at_eq, nonnegativity from domainCost_nonneg, and threshold positivity from canonicalThreshold_pos. No further tactic work; the certificate is just the packaged triple of those sibling results.
why it matters
Gives a single named certificate object for the nuclear-shell-from-J-cost development. Downstream consumers that need "the nuclear domain cost is a genuine cost with a positive threshold" can take this value rather than reassemble the three properties. It sits inside the Plan v7 structural theorem that the five shell-model orbital families match $\mathrm{configDim},D=5$, tying nuclear single-particle structure to the same J-cost geometry used elsewhere in Recognition Science (T5 J-uniqueness, RCL). No open sorry remains in this module; the certificate is the closed packaging step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.