twenty_is_magic
plain-language theorem explainer
The declaration establishes that 20 belongs to the explicit list of nuclear magic numbers generated by the phi-ladder. Nuclear modelers checking shell closures would cite it when confirming 8-tick periodicity in binding energies. The proof is a one-line computational decision that verifies membership in the list [2, 8, 20, 28, 50, 82, 126].
Claim. $20$ belongs to the set of nuclear magic numbers defined as the list $[2, 8, 20, 28, 50, 82, 126]$.
background
Nuclear binding energies in Recognition Science follow from the J-cost functional on the phi-lattice, with separate volume, surface, Coulomb, asymmetry, and pairing contributions. The module lists the seven magic numbers as [2, 8, 20, 28, 50, 82, 126] and attributes them to 8-tick shell structure, where 20 arises as 8 plus 12 passive edges. This rests on the upstream definition of magic_numbers and the eight-tick octave periodicity established in the unified forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic to check list membership by direct computation.
why it matters
The result supplies one verified entry in the magic-numbers list that the Nuclear.BindingEnergy module uses to connect 8-tick periodicity to nuclear shell structure. It supports the module's extension of the phi-ladder to binding energies and aligns with the T7 eight-tick octave landmark. No downstream theorems yet consume it, leaving open its integration into explicit binding-energy formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.