magic_numbers_contain_2
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 in Recognition Science
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.
scope and limits
- Does not derive the listed values from the J-cost functional equation or Recognition Composition Law.
- Does not prove that the enumerated set is complete or that no further magic numbers exist.
- Does not compute explicit J-cost values or defect distances for any entry.
- Does not connect the numbers to the mass formula, Berry creation threshold, or alpha band.
Lean usage
example : 2 ∈ magicNumbers := magic_numbers_contain_2formal statement (Lean)
36theorem magic_numbers_contain_2 : 2 ∈ magicNumbers := by decide
proof body
37