binding_per_nucleon
plain-language theorem explainer
Binding per nucleon is obtained by dividing the total binding energy expression by mass number A. Nuclear physicists modeling stability curves would cite this quantity to locate the iron peak and assess magic-number enhancements. The definition is a direct quotient applied to the volume, surface, Coulomb, and asymmetry terms assembled upstream.
Claim. The binding energy per nucleon is given by $B(A,Z)/A$, where $B(A,Z) = a_V A - a_S A^{2/3} - a_C Z(Z-1)/A^{1/3} - a_A (A-2Z)^2/(4A)$ and the coefficients $a_V,a_S,a_C,a_A,a_P$ are taken from the BindingCoefficients structure.
background
The module derives nuclear binding energies from the phi-ladder framework of Recognition Science. Nuclear binding is governed by the J-cost functional on the phi-lattice, producing five terms: volume saturation at nuclear scale, surface boundary cost, Coulomb electrostatic J-cost from alpha_EM, asymmetry from isospin imbalance, and pairing from 8-tick phase alignment. Magic numbers arise as 8-tick consequences (2, 8, 20, 28, ...).
proof idea
This is a one-line wrapper that divides the upstream binding_energy expression by the mass number A.
why it matters
The definition supports the module's structural claim that binding energy per nucleon peaks near A ≈ 56 (iron-56) with extra stability at magic numbers. It directly addresses question Q16 on deriving binding energies from the phi-ladder and connects to the eight-tick octave (T7) and D = 3 spatial dimensions (T8) in the forcing chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.