BindingCoefficients
plain-language theorem explainer
BindingCoefficients packages the five parameters of the liquid-drop model together with positivity constraints for use in phi-ladder derivations of nuclear binding. Nuclear physicists working inside Recognition Science cite the structure when evaluating volume, surface, Coulomb, asymmetry, and pairing contributions from J-cost on the phi-lattice. The declaration is a plain structure with five real fields and five positivity hypotheses carrying no computational content.
Claim. A structure consisting of five positive real numbers $a_V$, $a_S$, $a_C$, $a_A$, $a_P$ (in MeV) that represent the volume, surface, Coulomb, asymmetry, and pairing coefficients in the semi-empirical nuclear binding energy formula.
background
Nuclear binding in Recognition Science is governed by the J-cost functional on the phi-lattice. The module extends the already-verified 8-tick shell structure for magic numbers to continuous binding formulas, with the five terms arising as: volume from J-cost saturation at nuclear scale, surface from boundary J-cost, Coulomb from electrostatic alpha_EM, asymmetry from isospin imbalance, and pairing from 8-tick phase alignment. The upstream volume definition states that volume of a region equals the number of vertices, supplying the counting interpretation for the a_V term.
proof idea
This is a structure definition with no proof body. It declares the five coefficient fields and their positivity constraints directly.
why it matters
BindingCoefficients supplies the parameter record consumed by binding_energy and binding_per_nucleon. The concrete instance rs_binding_coefficients populates it with phi-powers scaled to observed MeV values, closing the link from the phi-ladder to nuclear data. It fills the Q16 question of whether binding energies follow from the same 8-tick and J-cost machinery that produces the magic numbers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.