NuclearShell3Cert
plain-language theorem explainer
Certificate structure that packages three J-cost properties for the nuclear shell derivation: diagonal vanishing of the domain cost, nonnegativity for positive mass and energy, and positivity of the canonical threshold. Cited by anyone assembling or inhabiting the nuclear-shell-from-J-cost certificate. Pure structure definition; no proof body.
Claim. A nuclear-shell certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; (ii) for all positive mass $m$ and energy $e$, $C(m,e)\ge 0$; (iii) the canonical threshold $T$ is strictly positive.
background
The module derives 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}$) from Recognition Science J-cost structure, identifying them with configuration dimension $\mathrm{configDim},D=5$. Status is structural: zero sorry, zero axiom.
The domain cost $C$ is the nuclear specialization of the recognition cost functional built from $J$. Upstream, cost_nonneg records that every recognition event has nonnegative cost via $J$-cost nonnegativity. The canonical threshold is the positive cutoff used to separate shell-level recognition events from the continuum.
This structure does not compute levels; it only names the three cost axioms the later certificate must discharge.
proof idea
No proof: the declaration is a structure whose three fields are propositions. Inhabitation is deferred to the sibling cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Those lemmas in turn rest on the foundation fact that recognition cost is nonnegative.
why it matters
Gives a single named type for the cost hypotheses needed by the nuclear-shell-from-J-cost pipeline. Downstream, cert builds a concrete inhabitant and cert_inhabited proves Nonempty NuclearShell3Cert, closing the structural certificate for the module.
In the RS forcing chain this sits under the nuclear application of J-cost uniqueness (T5) and the dimensional count that yields five orbital families once $D=3$ spatial dimensions and the configuration dimension are fixed. It does not itself prove magic numbers or binding energies; it only standardizes the cost interface those claims will cite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.