magic_20_from_cube
plain-language theorem explainer
The theorem states that the third magic number 20 equals 2 cubed plus three times 2 squared. Nuclear structure calculations inside the Recognition Science framework cite it to confirm the 8-tick shell closure for the phi-ladder. The proof reduces the equality to a direct numerical check via the norm_num tactic.
Claim. $20 = 2^3 + 3 · 2^2$
background
Nuclear binding energies in Recognition Science are obtained from the J-cost functional evaluated on the phi-lattice. The module verifies the seven magic numbers as direct consequences of 8-tick periodicity: 2 is the first shell, 8 completes one full period, and 20 is obtained by adding twelve passive edges to that period. The local setting extends this periodicity to the five terms of the semi-empirical mass formula (volume, surface, Coulomb, asymmetry, pairing) all expressed through J-cost saturation.
proof idea
The proof is a one-line wrapper that invokes the norm_num tactic to discharge the arithmetic identity by direct evaluation.
why it matters
This declaration supplies the twenty_from_cube field inside the NuclearBindingCert constructed by nuclear_binding_cert_exists. It completes the verification that the third magic number follows the 8-tick octave (T7) on the phi-ladder, as stated in the module documentation where 20 = 8 + 12. The result therefore anchors the claim that nuclear shell structure is governed by the same Recognition Composition Law that fixes the spatial dimension D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.