firstMagicNumber
plain-language theorem explainer
The declaration supplies the first nuclear magic number as the natural number 2. Nuclear physicists working inside the Recognition Science framework cite this constant when enumerating closed-shell proton and neutron counts. The definition is a direct constant assignment requiring no lemmas or computation.
Claim. The first nuclear magic number is the integer $2$.
background
The module NuclearPhysicsDepthFromRS places nuclear structure inside Recognition Science by identifying five force carriers and five structure categories that set configDim D = 5. Magic numbers mark closed shells and appear in the sequence 2, 8, 20, 28, 50, 82, 126. The supplied definition supplies the initial term, with the module note that 8 equals 2 cubed and that 82 lies below gap45 times 2.
proof idea
The declaration is a direct constant definition that assigns the value 2.
why it matters
This definition opens the enumeration of magic numbers in the B7 Nuclear section. It supplies the base term for the sequence whose next member satisfies 8 = 2^3, linking directly to the eight-tick octave (T7) of the forcing chain. The constant anchors later statements about nuclear binding peaks such as Fe-56 on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.