Pith. sign in
module module moderate

IndisputableMonolith.Nuclear.Nuclear_Shell_Gap_RS

show as:
view Lean formalization →

Module packaging the Recognition Science treatment of nuclear shell gaps via a domain cost and a canonical positive threshold. It exposes a certificate type `NuclearShellGapRS` with an inhabited witness, so nuclear phenomenology can sit on the same J-cost and Constants stack as the rest of the monolith. Argument structure is definitional plus elementary positivity and evaluation lemmas, not a deep derivation.

claimThe module defines a nuclear-domain cost $C_{\mathrm{nuc}}$, proves $C_{\mathrm{nuc}}\ge 0$ and an evaluation identity at a point, introduces a canonical threshold $\theta>0$, and packages these into a certificate type for the RS nuclear shell-gap claim, shown to be inhabited.

background

Recognition Science measures mismatch with the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the Recognition Composition Law. Constants supplies the RS-native tick $\tau_0=1$ and the golden-ratio ladder used across mass and coupling formulae. Cost is the shared cost layer imported here.

Nuclear shell gaps are the large energy spacings at magic nucleon numbers. In this module they are not derived from a full many-body Hamiltonian; they are encoded as a domain-specific cost together with a positive canonical threshold that marks when a gap is recognized as shell-closed in RS units.

Sibling objects named in the module include domainCost (and its evaluation and nonnegativity facts), canonicalThreshold (with positivity), and the certificate bundle NuclearShellGapRS with cert / cert_inhabited.

proof idea

Definition-heavy module. Domain cost and canonical threshold are introduced as defs; nonnegativity and positivity are short analytic or algebraic facts on those defs; evaluation-at-a-point is an identity lemma. The certificate is a structure packing the cost/threshold data, discharged by an inhabited instance rather than a long tactic proof. No forcing-chain (T0–T8) steps are proved here.

why it matters in Recognition Science

Places nuclear shell structure on the same cost-and-certificate pattern used elsewhere in the monolith (Constants + Cost), so nuclear phenomenology can be cited beside particle and coupling results without a separate metatheory. Downstream use is not yet wired in this graph (used_by empty); the module is an entry point for nuclear-domain claims rather than a leaf of the T5–T8 forcing chain. It does not itself force $D=3$, the eight-tick octave, or the $\alpha^{-1}$ band.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)