rs_binding_coefficients
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.