magicNumbers
plain-language theorem explainer
The definition lists the nuclear magic numbers as the finite set of natural numbers 2, 8, 20, 28, 50, 82, 126. Nuclear physicists applying Recognition Science would reference this enumeration to verify shell closures at J-cost minima on the recognition lattice. The declaration proceeds by direct listing of the standard sequence with no further computation.
Claim. The set of nuclear magic numbers is the finite subset $S = {2, 8, 20, 28, 50, 82, 126}$ of the natural numbers.
background
Nuclear magic numbers correspond to gaps in the shell-model energy spectrum at J-cost minima on the nuclear recognition lattice. The module establishes the local setting by linking specific entries to the eight-tick period: 2 equals 2 to the first power as the minimum magic number, and 8 equals 2 cubed as the 8-tick octave when spatial dimensions equal 3. This supplies the concrete list for subsequent certification without upstream dependencies.
proof idea
The declaration is a direct definition by explicit enumeration of the set elements. No lemmas or tactics are invoked beyond the literal finite-set constructor.
why it matters
This definition provides the list that populates the NuclearMagicCert structure and supports the cardinality result of seven elements. It realizes the framework landmark that 8 equals 2 to the power 3 matching the eight-tick period at three dimensions from the unified forcing chain. The enumeration closes the basic verification step for membership of 2 and 8 in the magic set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.