magic_2_eq_2pow1
plain-language theorem explainer
The equality 2 = 2^1 identifies the smallest magic number in the Recognition Science treatment of nuclear shell closures. Nuclear modelers using the phi-ladder gaps would cite this base case when listing the sequence 2, 8, 20, 28, 50, 82, 126. The proof is a direct decision on natural-number arithmetic.
Claim. $2 = 2^1$ holds as the minimum magic number on the nuclear recognition lattice.
background
Nuclear magic numbers in Recognition Science are defined as gaps in the shell-model energy spectrum at J-cost minima on the nuclear recognition lattice. The module states the sequence 2, 8, 20, 28, 50, 82, 126, noting that 2 equals 2 to the first power as the base entry while 8 equals 2 cubed matches the eight-tick period. This theorem supplies the explicit equality for the minimal term.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the natural-number equality.
why it matters
This base equality anchors the enumeration of magic numbers in the RS nuclear model and connects to the T7 eight-tick octave where higher terms satisfy 8 = 2^D. It supports the module claim that magic numbers arise from phi-ladder gaps, with 2 as the starting point before the D = 3 spatial dimension enters for the period-8 term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.