magic_numbers_sorted
plain-language theorem explainer
The list of seven nuclear magic numbers is strictly increasing. Nuclear modelers in the Recognition Science framework cite this to confirm the ordered sequence of 8-tick shell closures before constructing binding-energy certificates. The proof is a single decision tactic that checks the property on the explicit list.
Claim. The list $[2, 8, 20, 28, 50, 82, 126]$ is strictly sorted under the natural order on the natural numbers.
background
The Nuclear Binding Energy module derives nuclear properties from the phi-ladder and J-cost functional. Magic numbers are introduced as 8-tick shell closures: 2 = 2^1, 8 = 2^3, 20 = 8 + 12, 28 = 20 + 8, with 50, 82, 126 following from spin-orbit splitting. The upstream definition supplies the concrete list [2, 8, 20, 28, 50, 82, 126] whose ordering is required for later certification steps.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the fixed list and the standard less-than relation.
why it matters
This supplies the sortedness field to nuclear_binding_cert_exists, which assembles the full binding-energy certificate including seven_magic, eight_from_cube, and coefficients_positive. It closes a verification step in the 8-tick periodicity analysis of nuclear shells and connects directly to the T7 landmark of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.