nuclear_binding_cert_exists
plain-language theorem explainer
The declaration proves existence of a NuclearBindingCert recording that seven magic numbers are present and sorted, that 8 equals 2 cubed and 20 equals 8 plus 12, and that the volume, surface, and Coulomb coefficients are positive. Nuclear modelers using the phi-ladder would cite it to confirm the binding energy decomposition is well-defined. The proof is a direct term that assembles the required record from the magic-number lemmas and the coefficient definition.
Claim. There exists a certificate $C$ such that the magic-number list $M$ satisfies $|M|=7$, $M$ is strictly increasing, $8=2^3$, $20=2^3+3·2^2$, and the volume, surface, and Coulomb coefficients satisfy $a_V>0$, $a_S>0$, $a_C>0$.
background
The module treats nuclear binding as governed by the J-cost functional on the phi-lattice. The binding energy per nucleon decomposes into a volume term from J-cost saturation, a surface term from boundary costs on the lattice, a Coulomb term from the electromagnetic coupling, an asymmetry term from isospin imbalance, and a pairing term from 8-tick phase alignment. Magic numbers are presented as direct consequences of 8-tick periodicity: 2 as the first complete shell, 8 as one full period, 20 as 8 plus passive edges, and 28 as double closure. The theorem depends on four upstream results inside the module: magic_numbers_count and magic_numbers_sorted established by direct decision, magic_8_from_cube and magic_20_from_cube established by norm_num, together with the definition rs_binding_coefficients that supplies the three positive leading coefficients from explicit powers of phi.
proof idea
The proof is a single-term construction of the NuclearBindingCert record. It supplies the seven_magic field directly from magic_numbers_count, the magic_sorted field from magic_numbers_sorted, the eight_from_cube field from magic_8_from_cube, the twenty_from_cube field from magic_20_from_cube, and the coefficients_positive field by selecting the three positivity conjuncts from rs_binding_coefficients.
why it matters
The theorem certifies the NuclearBindingCert structure that anchors the binding-energy model inside the Recognition Science framework. It links the eight-tick octave (T7) to the observed magic numbers and guarantees that the leading coefficients remain positive, as required by J-cost saturation on the phi-ladder. The certificate supplies the minimal data needed for any later derivation of binding energies per nucleon, although no downstream theorem yet consumes it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.