magicNumbersCard
Recognition Science identifies seven nuclear magic numbers as the complete list of gaps at J-cost minima on the recognition lattice. Nuclear structure modelers working inside the RS framework cite this cardinality to confirm the sequence 2, 8, 20, 28, 50, 82, 126 matches the eight-tick octave at D=3. The proof is a direct decide computation on the explicit Finset definition of magicNumbers.
claimThe set of nuclear magic numbers $M = {2, 8, 20, 28, 50, 82, 126}$ satisfies $|M| = 7$.
background
The module NuclearMagicNumbersFromRS defines magicNumbers as the Finset {2, 8, 20, 28, 50, 82, 126}. These values mark gaps in the shell-model energy spectrum at J-cost minima, with the explicit note that 8 equals 2 cubed and equals the 8-tick period. The upstream tick definition supplies the fundamental RS time quantum τ₀ = 1, while period(k) := phi^k encodes the self-similar scaling. The local setting treats 2 as the minimum magic number and 8 as the signature of the eight-tick octave at three spatial dimensions.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the explicit Finset definition of magicNumbers, which evaluates its cardinality as 7.
why it matters in Recognition Science
This theorem supplies the seven_magic field inside the NuclearMagicCert structure that certifies the full list of magic numbers. It anchors the framework claim that 8 arises as the 8-tick period at D=3 and closes the enumeration step in the nuclear-magic sequence without additional hypotheses.
scope and limits
- Does not derive the listed values from the J-cost function.
- Does not prove these are the only magic numbers observed in nuclei.
- Does not address experimental mass or binding-energy deviations.
- Does not connect the list to the mass formula or alpha band.
Lean usage
example : magicNumbers.card = 7 := magicNumbersCardformal statement (Lean)
26theorem magicNumbersCard : magicNumbers.card = 7 := by decide
proof body
Term-mode proof.
27
28/-- 8 = 2^3 = 8-tick period at D=3. -/