magic_numbers
plain-language theorem explainer
The declaration supplies the list of nuclear magic numbers 2, 8, 20, 28, 50, 82, 126 as the basis for shell closures in the Recognition Science nuclear model. Researchers deriving binding energies from the phi-ladder would reference this enumeration when checking eight-tick periodicity. It is introduced as a direct list definition with no computation.
Claim. The magic numbers are the list $ [2, 8, 20, 28, 50, 82, 126] $.
background
The module Nuclear Binding Energy from the φ-Ladder asks whether binding energies can be derived from the phi-ladder framework. Magic numbers arise from 8-tick periodicity on the φ-lattice: 2 equals 2¹ as the first complete shell, 8 equals 2³ as one full period, with 20, 28 and higher numbers following from spin-orbit splitting. Nuclear binding follows the J-cost functional with volume, surface, Coulomb, asymmetry and pairing terms.
proof idea
The declaration is a direct definition that enumerates the seven numbers. Downstream results invoke it through membership and length checks.
why it matters
It supplies the input list for theorems such as eight_is_magic and the NuclearBindingCert structure, which records seven_magic and magic_sorted properties. The module connects these numbers to the eight-tick octave (T7) and D = 3 dimensions in the forcing chain. It closes the shell structure step before extending to binding energy coefficients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.