Nuclear Binding Energy Volume Dominates Surface

The volume term

The binding energy of an atomic nucleus is the energy that holds its protons and neutrons together. A standard way to estimate it, the semi-empirical mass formula, splits the total into competing terms. The volume term grows with the number of nucleons A, the surface term grows with the surface area, roughly A to the two-thirds power. For a large enough nucleus, the volume term must win: there are simply more interior nucleons than surface nucleons, and each interior one contributes fully to the binding.

The machine-checked library of formal theorems proves this ordering as a general statement. Its theorem volume_dominates_surface says that for any positive nucleon number A (at least 1), and any choice of coefficients where the surface coefficient is smaller than the volume coefficient, the volume contribution strictly exceeds the surface contribution. In symbols, a_V * A > a_S * A^(2/3). The proof needs no special numbers: it follows from the arithmetic of exponents and the assumption that a_S < a_V. The framework's own coefficients, built from the golden ratio phi, satisfy that condition, so the inequality holds for its proposed nuclear model.

What the theorem does not claim is just as important. It does not prove that the volume term dominates the Coulomb or asymmetry terms, which also appear in the mass formula. It does not say anything about the numerical size of the binding energy, only that one term is larger than another. And it does not establish that the volume term dominates for all A; the statement requires A to be at least 1, which is a mild condition but still a condition.

The practical consequence is structural. The dominance of the volume term is what makes binding energy per nucleon roughly constant for medium and heavy nuclei, and it is why the curve of binding energy is so flat in the middle of the periodic table. The theorem pins down that flatness as a formal consequence of the coefficient ordering, not as a lucky accident of one particular set of numbers.

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

noncomputable def rs_binding_coefficients : BindingCoefficients where
  a_V := phi ^ 3 * 1.05
  a_S := phi ^ 3 * 0.77
  a_C := phi * 0.44
  a_A := phi ^ 3 * 1.55
  a_P := phi ^ 2 * 4.5
  h_V_pos := mul_pos (pow_pos phi_pos 3) (by norm_num)
  h_S_pos := mul_pos (pow_pos phi_pos 3) (by norm_num)
  h_C_pos := mul_pos phi_pos (by norm_num)
  h_A_pos := mul_pos (pow_pos phi_pos 3) (by norm_num)
  h_P_pos := mul_pos (pow_pos phi_pos 2) (by norm_num)

What this page does not claim

The theorem does not prove that the volume term dominates the Coulomb or asymmetry terms. The theorem does not establish that the volume term dominates for all A, only for A at least 1. The theorem does not give the numerical size of the binding energy, only the ordering of two terms.

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: