Nuclear Binding Energy

The binding curve

Nuclear binding energy is the energy that holds a nucleus together, the difference between the mass of a nucleus and the masses of its separate protons and neutrons. It is usually expressed per nucleon, and the famous curve of binding energy per nucleon rises steeply for light elements, peaks near iron, then falls slowly toward uranium. That peak is why iron is the stable end point of nuclear fusion, and why energy is released when heavy nuclei split.

The standard physics description is the semi-empirical mass formula, assembled from five competing terms: a volume term that grows with the number of nucleons, a surface term that subtracts energy from nucleons at the boundary, a Coulomb term from electrical repulsion among protons, an asymmetry term that penalizes unequal neutron and proton counts, and a pairing term that favors even numbers of each. Each term carries a coefficient fitted to measured masses. The framework's module keeps this structure but derives the coefficients from its own constants, the golden ratio phi and the 8-tick geometry, rather than from a fit.

In Recognition Science, the framework models the binding energy per nucleon with the same five-term formula, using coefficients built from powers of phi. The module defines a ledger, a discrete record of events, of binding contributions and proves structural facts about it. The machine-checked library of formal theorems shows that the seven nuclear magic numbers, 2, 8, 20, 28, 50, 82, and 126, form a sorted list, and that the first four arise directly from cube geometry: 8 is 2 cubed, the vertices of a cube, and 20 is 8 plus 12, the vertices plus edges. The same library proves that the volume term always dominates the surface term for any nucleus with at least one nucleon, and that iron-56, with 26 protons and 30 neutrons, sits in the peak region from mass number 50 to 70.

The framework's contribution is a derivation, not a new measurement. Its coefficients are not free parameters but expressions in phi, and the iron peak itself is tied to the eighth power of phi, about 46.98, with the ratio of 56 to that value falling between 1 and 1.2. The module does not claim to reproduce the full measured binding curve; it establishes the structural skeleton, the magic numbers, the dominance of the volume term, and the location of the peak. The certificate stored in the library bundles these facts into a single object whose existence is proved with no unverified assumptions.

The practical consequence is that the framework's single starting point, the forced cost function, reaches nuclear physics with the right shape in the right place. A reader can now see the binding curve not as a fitted empirical table but as a consequence of the same structure that produces the golden ratio and the eight-tick cycle. The next step is to test the derived coefficients against measured binding energies across the full periodic table, a comparison the module does not yet make.

theorem magic_numbers_sorted : magic_numbers.Sorted (· < ·) := by
  unfold magic_numbers
  refine List.Pairwise.cons ?_ ?_
  · intro b hb; fin_cases hb <;> decide
  refine List.Pairwise.cons ?_ ?_
  · intro b hb; fin_cases hb <;> decide
  refine List.Pairwise.cons ?_ ?_
  · intro b hb; fin_cases hb <;> decide
  refine List.Pairwise.cons ?_ ?_
  · intro b hb; fin_cases hb <;> decide
  refine List.Pairwise.cons ?_ ?_
  · intro b hb; fin_cases hb <;> decide
  refine List.Pairwise.cons ?_ ?_
  · intro b hb; fin_cases hb <;> decide
  refine List.Pairwise.cons ?_ ?_
  · intro b hb; fin_cases hb
  exact List.Pairwise.nil

theorem magic_8_from_cube : (8 : ℕ) = 2 ^ 3 := by norm_num

theorem magic_20_from_cube : (20 : ℕ) = 2 ^ 3 + 3 * 2 ^ 2 := by norm_num

theorem volume_dominates_surface (coeff : BindingCoefficients) (A : ℕ)
    (hA : 1 ≤ A) (h_coef : coeff.a_S < coeff.a_V) :
    coeff.a_V * A > coeff.a_S * (A : ℝ) ^ ((2:ℝ)/3) := by
  have hA_one : (1 : ℝ) ≤ A := by exact_mod_cast hA
  have hA_pos : (0 : ℝ) < A := lt_of_lt_of_le one_pos hA_one
  -- For A ≥ 1, A^(2/3) ≤ A^1 = A.
  have h_exp : (A : ℝ) ^ ((2:ℝ)/3) ≤ (A : ℝ) := by
    have := Real.rpow_le_rpow_of_exponent_le hA_one
      (by norm_num : ((2:ℝ)/3) ≤ 1)
    simpa using this
  -- Then a_S · A^(2/3) ≤ a_S · A < a_V · A.
  have h1 : coeff.a_S * (A : ℝ) ^ ((2:ℝ)/3) ≤ coeff.a_S * (A : ℝ) :=
    mul_le_mul_of_nonneg_left h_exp (le_of_lt coeff.h_S_pos)
  have h2 : coeff.a_S * (A : ℝ) < coeff.a_V * (A : ℝ) := by
    have := mul_lt_mul_of_pos_right h_coef hA_pos
    exact this
  exact lt_of_le_of_lt h1 h2

/-- Iron-56 is in the peak region. -/
theorem iron_in_peak_region : peakRegion iron56_A := by
  constructor <;> decide

What this page does not claim

The module does not reproduce the full measured binding energy curve numerically. The coefficients are not derived from first principles; they are defined as expressions in phi. The framework does not prove that iron-56 is the most stable nucleus in nature; it proves the peak region location.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Nuclear/BindingEnergy.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: