magic_numbers_count
The list of nuclear magic numbers is confirmed to contain exactly seven entries. Nuclear physicists extending the phi-ladder model to binding energies would cite this cardinality to fix the shell count before assembling the full binding certificate. The verification is a one-line decision procedure that evaluates the concrete list length directly.
claimThe list of nuclear magic numbers has cardinality seven: $|[2, 8, 20, 28, 50, 82, 126]| = 7$.
background
Recognition Science derives nuclear binding from the J-cost functional on the phi-ladder. The module lists the seven magic numbers as the explicit sequence [2, 8, 20, 28, 50, 82, 126] and traces them to eight-tick periodicity: 2 = 2^1, 8 = 2^3, 20 = 8 + 12, 28 = 20 + 8, with the remaining three following from spin-orbit splitting. The local setting is the extension of the eight-tick octave (T7) to nuclear shell structure, with binding terms (volume, surface, Coulomb, asymmetry, pairing) expressed via J-cost saturation and alpha_EM.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality on the concrete list length.
why it matters in Recognition Science
This cardinality is invoked inside nuclear_binding_cert_exists to supply the seven_magic field of NuclearBindingCert. It thereby anchors the count of magic numbers that the module attributes to the eight-tick octave before the binding energy coefficients are certified. The result closes one step in the extension from the forcing chain (T5-T8) to nuclear observables while leaving the explicit derivation of the larger magic numbers (50, 82, 126) for later work.
scope and limits
- Does not derive the numerical values of the magic numbers from the phi-ladder axioms.
- Does not prove that these numbers produce observed nuclear shell closures.
- Does not compute any binding energy values or coefficients.
- Does not address the physical stability or decay properties of the listed nuclei.
formal statement (Lean)
46theorem magic_numbers_count : magic_numbers.length = 7 := by decide
proof body
47