two_is_magic
plain-language theorem explainer
The declaration confirms that 2 belongs to the list of nuclear magic numbers generated by 8-tick periodicity on the phi-ladder. Nuclear structure theorists would cite it as the base case for shell closures in the Recognition Science model of binding energies. The proof is a one-line decision procedure that checks explicit list membership.
Claim. $2$ belongs to the list of nuclear magic numbers defined as $[2, 8, 20, 28, 50, 82, 126]$.
background
The Nuclear Binding Energy module derives magic numbers from 8-tick periodicity on the phi-ladder, where nuclear binding follows the J-cost functional with volume, surface, Coulomb, asymmetry, and pairing terms. The upstream definition supplies the explicit list magic_numbers := [2, 8, 20, 28, 50, 82, 126] as the seven standard shell closures. This list encodes the first complete shell at 2, one full 8-tick period at 8, and subsequent closures at 20, 28, 50, 82, 126.
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify membership of 2 in the magic_numbers list.
why it matters
This supplies the initial instance of the magic-number sequence required by the module's 8-tick shell structure for nuclear binding energies. It directly supports the framework landmark T7 eight-tick octave and the claim that magic numbers are 8-tick consequences. The declaration closes the base case for the parent list definition while leaving open the derivation of explicit binding-energy coefficients from the J-cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.