eight_is_magic
Eight belongs to the list of nuclear magic numbers generated by the phi-ladder model. Nuclear physicists extending the Recognition Science framework to shell structure would cite this to anchor the eight-tick periodicity. The proof is a one-line decision tactic that checks membership against the fixed list definition.
claim$8$ belongs to the set of nuclear magic numbers arising from eight-tick shell closures on the phi-ladder, where the set is defined as $[2, 8, 20, 28, 50, 82, 126]$.
background
The module examines whether nuclear binding energies follow from the phi-ladder. Binding is controlled by the J-cost functional on the phi-lattice, producing volume, surface, Coulomb, asymmetry, and pairing terms. Magic numbers are presented as eight-tick consequences: 2 marks the first complete shell and 8 marks one full period.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the membership predicate against the upstream list definition.
why it matters in Recognition Science
The result confirms the second magic number as an eight-tick closure, supporting the module's extension from shell structure to binding energies. It directly instantiates the eight-tick octave landmark and the claim that the seven magic numbers are 8-tick consequences. No downstream theorems yet reference it.
scope and limits
- Does not derive the list from the J-cost functional or first principles.
- Does not calculate any binding energies or coefficients.
- Does not treat spin-orbit splitting for the higher magic numbers 50, 82, 126.
formal statement (Lean)
51theorem eight_is_magic : 8 ∈ magic_numbers := by decide