NuclearBindingCert
plain-language theorem explainer
NuclearBindingCert is a record structure that bundles five propositions: the magic-number list has length exactly 7 and is strictly increasing, 8 equals 2 cubed while 20 equals 2 cubed plus three times 2 squared, and the volume, surface, and Coulomb coefficients in the RS binding model are all positive. Nuclear theorists working inside the Recognition Science framework cite it to certify that the phi-ladder supplies the observed shell closures and leading terms of the semi-empirical mass formula. The declaration is a plain structure definition;
Claim. A certificate structure asserting that the list of nuclear magic numbers has length 7 and is strictly increasing, that $8=2^3$ and $20=2^3+3·2^2$, and that the volume, surface, and Coulomb coefficients $a_V$, $a_S$, $a_C$ in the Recognition Science binding model are all positive.
background
The module derives nuclear binding energies from the J-cost functional on the phi-lattice. Magic numbers are defined as the list [2, 8, 20, 28, 50, 82, 126] and are already shown to arise from 8-tick periodicity. The binding coefficients are given by the noncomputable definition rs_binding_coefficients whose fields are a_V := phi^3 * 1.05, a_S := phi^3 * 0.77, a_C := phi * 0.44 together with the asymmetry and pairing terms. The local setting is the question whether binding energies follow from the same phi-ladder that forces D=3 and the eight-tick octave.
proof idea
The declaration is a structure definition that directly assembles the five field propositions; no lemmas or tactics are applied.
why it matters
The structure is the hypothesis interface for the existence theorem nuclear_binding_cert_exists, which shows the record is inhabited. It therefore anchors the module's claim that the seven magic numbers and the leading binding coefficients are consistent with the J-cost saturation, boundary cost, and electrostatic term on the phi-ladder, closing the Q16 derivation step that links nuclear structure to the eight-tick periodicity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.