eight_is_magic
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.