magicNumbersCard
plain-language theorem explainer
The nuclear magic numbers set in Recognition Science has cardinality seven. Nuclear structure researchers citing the RS shell-model gaps would reference this result when confirming the listed closures. The proof is a direct decidable computation on the explicit Finset definition.
Claim. The finite set $S = {2, 8, 20, 28, 50, 82, 126}$ satisfies $|S| = 7$.
background
The module defines nuclear magic numbers as gaps in the shell-model energy spectrum at J-cost minima on the nuclear recognition lattice, with explicit values 2, 8, 20, 28, 50, 82, 126. The module states that 8 equals 2 cubed, matching the 8-tick period at D=3, and 2 is the minimum magic number. Upstream, the magicNumbers definition supplies the Finset, while tick is the fundamental RS time quantum equal to 1 and period(k) equals phi to the k.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the explicit Finset cardinality equality.
why it matters
This result populates the seven_magic field of the NuclearMagicCert definition. It anchors the module's claim that 8 equals the 8-tick octave (T7) at D=3 in the forcing chain. The module doc quotes the relation 8 = 2^D as the most notable feature linking to the Recognition Composition Law and phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.