nuclear_binding_cert_exists
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.
claimThere 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 in Recognition Science
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.
scope and limits
- Does not compute numerical binding energies for any specific nucleus.
- Does not derive the asymmetry or pairing coefficients.
- Does not obtain the magic numbers from the Recognition Composition Law.
- Does not address experimental calibration of the coefficient values.
formal statement (Lean)
129theorem nuclear_binding_cert_exists : Nonempty NuclearBindingCert :=
proof body
Term-mode proof.
130 ⟨{ seven_magic := magic_numbers_count
131 magic_sorted := magic_numbers_sorted
132 eight_from_cube := magic_8_from_cube
133 twenty_from_cube := magic_20_from_cube
134 coefficients_positive := ⟨rs_binding_coefficients.h_V_pos,
135 rs_binding_coefficients.h_S_pos, rs_binding_coefficients.h_C_pos⟩ }⟩
136
137end
138
139end IndisputableMonolith.Nuclear.BindingEnergy