pith. machine review for the scientific record. sign in
def definition def or abbrev high

binding_energy

show as:
view Lean formalization →

Nuclear binding energies are expressed in this definition as the sum of volume, surface, Coulomb, and asymmetry contributions scaled by coefficients from the phi-ladder J-cost. Researchers extending the semi-empirical mass formula to Recognition Science would reference this when verifying predictions against measured nuclear masses. The implementation directly assembles the four terms using a let-binding for neutron number and power-law scalings for surface and Coulomb effects.

claimLet $a_V, a_S, a_C, a_A$ denote the volume, surface, Coulomb, and asymmetry coefficients supplied by a BindingCoefficients record. The binding energy of a nucleus with mass number $A$ and proton number $Z$ is then $E_b = a_V A - a_S A^{2/3} - a_C Z(Z-1)/A^{1/3} - a_A (A-2Z)^2/(4A)$ in MeV.

background

In the Nuclear.BindingEnergy module, nuclear binding is derived from the J-cost functional on the phi-lattice as described in the module documentation. The BindingCoefficients structure supplies the four coefficients a_V (volume saturation), a_S (surface boundary cost), a_C (Coulomb electrostatic J-cost from alpha_EM), and a_A (asymmetry from isospin imbalance). Upstream results include the active edge count A from IntegrationGap and Anchor, and the actualization operator A from Modal.Actualization, which together enforce the phi-power balance at D=3. The module verifies the seven magic numbers as 8-tick consequences before extending to binding energies.

proof idea

This is a direct definition that computes the binding energy by first setting N := A - Z and then evaluating the standard four-term expression using the supplied coefficients and real-number powers. No lemmas are applied beyond the arithmetic operations; it serves as a one-line wrapper that assembles the volume, surface, Coulomb, and asymmetry terms.

why it matters in Recognition Science

This definition supplies the core binding energy expression used by the downstream binding_per_nucleon function, which computes energy per nucleon and notes its peak near iron. It realizes the RS approach to nuclear binding outlined in the module documentation, linking the volume term to J-cost saturation, surface to boundary costs, and Coulomb to alpha_EM, all within the eight-tick periodicity framework (T7). It closes part of the extension from magic numbers to full binding energies, leaving the pairing term (a_P) and explicit coefficient derivation as open extensions.

scope and limits

Lean usage

noncomputable def binding_per_nucleon (coeff : BindingCoefficients) (A Z : ℕ) : ℝ := binding_energy coeff A Z / A

formal statement (Lean)

  97noncomputable def binding_energy (coeff : BindingCoefficients) (A Z : ℕ) : ℝ :=

proof body

Definition body.

  98  let N := A - Z
  99  coeff.a_V * A - coeff.a_S * (A : ℝ) ^ ((2:ℝ)/3) -
 100  coeff.a_C * Z * (Z - 1) / (A : ℝ) ^ ((1:ℝ)/3) -
 101  coeff.a_A * ((N : ℝ) - Z) ^ 2 / (4 * A)
 102

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.