magic_numbers_contain_2
plain-language theorem explainer
Recognition Science identifies 2 as the smallest nuclear magic number arising at a J-cost minimum on the recognition lattice. Nuclear structure physicists would cite the result when confirming the base case of the observed shell closures 2, 8, 20, 28, 50, 82, 126. The proof is a one-line decision procedure that checks explicit membership in the finite enumerated set.
Claim. $2$ belongs to the set of nuclear magic numbers, the Finset containing $2, 8, 20, 28, 50, 82, 126$, each identified as a gap at a J-cost minimum on the nuclear recognition lattice.
background
The module NuclearMagicNumbersFromRS treats nuclear magic numbers as gaps in the shell-model energy spectrum that occur at J-cost minima on the nuclear recognition lattice. The upstream definition supplies the explicit Finset magicNumbers := {2, 8, 20, 28, 50, 82, 126}. Module documentation notes that 2 equals 2^1 and serves as the minimum magic number, while 8 equals 2^3 and matches the eight-tick period.
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify membership of 2 in the explicitly enumerated set magicNumbers.
why it matters
The theorem populates the has_2 field inside the NuclearMagicCert record that assembles all verified properties of the magic-number list. It anchors the lower end of the sequence, consistent with the framework's eight-tick octave (T7) and the base of the phi-ladder. The module documentation explicitly flags 2 as the minimum magic number and 8 as 2^D with D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.