magic_20_from_cube
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 in Recognition Science
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.
scope and limits
- Does not derive numerical binding energies for any nucleus.
- Does not prove why twelve passive edges appear after the first 8-tick shell.
- Does not address spin-orbit splitting for higher magic numbers.
- Does not connect the arithmetic identity to the J-cost functional.
Lean usage
twenty_from_cube := magic_20_from_cubeformal statement (Lean)
65theorem magic_20_from_cube : (20 : ℕ) = 2 ^ 3 + 3 * 2 ^ 2 := by norm_num