rs_binding_coefficients
rs_binding_coefficients supplies the five coefficients of the semi-empirical nuclear binding formula as explicit multiples of powers of phi, scaled to observed MeV scales. Nuclear theorists using the Recognition Science framework cite these values when computing binding energies from J-cost saturation on the phi-lattice. The definition is a direct record construction whose five positivity fields are discharged by the positivity tactic.
claimThe binding coefficients are the record with volume term $a_V = phi^3 * 1.05$, surface term $a_S = phi^3 * 0.77$, Coulomb term $a_C = phi * 0.44$, asymmetry term $a_A = phi^3 * 1.55$, and pairing term $a_P = phi^2 * 4.5$, each required to be positive.
background
Nuclear binding energies are obtained from the J-cost functional on the phi-lattice. The volume term follows from saturation of recognition cost inside a filled shell; the surface term from boundary defects; the Coulomb term from electrostatic cost tied to alpha_EM; the asymmetry term from isospin imbalance; and the pairing term from 8-tick phase alignment. The module states that the seven magic numbers already arise as 8-tick consequences and extends the same lattice to binding coefficients. Upstream, cost is the derived J-cost of a multiplicative recognizer comparator, phase(k) returns the k-th multiple of pi/4 for k in Fin 8, and tick is the unit time quantum.
proof idea
The declaration is a direct record construction that populates the five real fields with the listed phi-powers and numerical prefactors. Each positivity field is discharged by a one-line application of the positivity tactic.
why it matters in Recognition Science
This definition populates the coefficients_positive field of NuclearBindingCert and is invoked by nuclear_binding_cert_exists. It supplies the concrete numbers needed to close the nuclear-binding extension of the phi-ladder after the magic-number results (T7 eight-tick octave). The construction directly implements the five-term decomposition listed in the module doc-comment for Q16.
scope and limits
- Does not derive the numerical prefactors from the J-cost functional; they are inserted by hand.
- Does not compute binding energies for specific nuclei.
- Does not prove that these coefficients reproduce the full experimental binding curve.
- Does not address spin-orbit corrections beyond the listed pairing term.
formal statement (Lean)
85noncomputable def rs_binding_coefficients : BindingCoefficients where
86 a_V := phi ^ 3 * 1.05 -- ≈ 15.7 MeV (volume, from J-cost saturation)
proof body
Definition body.
87 a_S := phi ^ 3 * 0.77 -- ≈ 11.5 MeV (surface, boundary J-cost)
88 a_C := phi * 0.44 -- ≈ 0.71 MeV (Coulomb, from α_EM)
89 a_A := phi ^ 3 * 1.55 -- ≈ 23.2 MeV (asymmetry, isospin cost)
90 a_P := phi ^ 2 * 4.5 -- ≈ 11.8 MeV (pairing, 8-tick phase)
91 h_V_pos := by positivity
92 h_S_pos := by positivity
93 h_C_pos := by positivity
94 h_A_pos := by positivity
95 h_P_pos := by positivity
96