canonicalThreshold
plain-language theorem explainer
Defines the canonical real threshold as φ − 3/2 in RS-native units for the nuclear shell model built from J-cost. Anyone comparing single-particle domain costs against a fixed cutoff in this module cites it. The body is a one-line arithmetic definition; no proof obligations.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden-ratio fixed point of Recognition Science.
background
The module derives nuclear shell single-particle structure from the J-cost. In RS, the unique cost is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced by the Recognition Composition Law and the T5 uniqueness step. The golden ratio $\varphi$ is the self-similar fixed point (T6).
Local setting: five canonical orbital families $s_{1/2}, p_{1/2}, p_{3/2}, d_{3/2}, d_{5/2}$ are identified with configuration dimension $D=5$. Domain costs on those families are compared to a fixed real cutoff; that cutoff is this constant.
Sibling facts in the same file establish nonnegativity of the domain cost and positivity of the threshold, then package a certificate that the five-shell picture sits above the cutoff.
proof idea
Pure definition: the real constant is written as $\varphi - 3/2$ with no lemmas or tactics. Downstream positivity and certificate lemmas unfold this abbreviation and reason about the resulting arithmetic value.
why it matters
Gives the module a single named RS-native cutoff against which nuclear domain costs are judged. It sits under the structural claim that the five shell families equal configDim $D=5$, with zero sorry and zero axioms in the file. The value is built from $\varphi$ (T6) rather than an empirical MeV scale, so the shell comparison stays inside the same unit system as $c=1$, $\hbar=\varphi^{-5}$, and the mass ladder. No parent theorems are listed on the dependency graph; the immediate consumers are the positivity lemma and the NuclearShell3 certificate in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.