magic_numbers_contain_8
plain-language theorem explainer
The theorem confirms that 8 belongs to the finite set of nuclear magic numbers. Nuclear physicists modeling shell structure in the Recognition Science framework would cite it when linking the observed magic number 8 to the eight-tick period. The proof is a direct decision procedure that verifies membership in the explicitly listed Finset.
Claim. The integer 8 is an element of the nuclear magic numbers set defined by $8, 2, 20, 28, 50, 82, 126$.
background
In the Recognition Science framework, nuclear magic numbers are gaps in the shell-model energy spectrum at J-cost minima on the nuclear recognition lattice. The module defines the set explicitly as the Finset containing 2, 8, 20, 28, 50, 82, and 126, with 8 identified as 2 cubed corresponding to the eight-tick octave period and D = 3 spatial dimensions. This theorem rests on the upstream definition of magicNumbers as that concrete collection of natural numbers.
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify set membership for the finite Finset of natural numbers.
why it matters
This result supplies the has_8 field inside the NuclearMagicCert structure that aggregates certificates for all listed magic numbers. It directly supports the module's emphasis on 8 as 2^D from the T7 eight-tick octave in the UnifiedForcingChain. The declaration closes a simple membership check that feeds the broader certification of RS-derived nuclear numbers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.