binding_per_nucleon

formal source

 100  coeff.a_C * Z * (Z - 1) / (A : ℝ) ^ ((1:ℝ)/3) -
 101  coeff.a_A * ((N : ℝ) - Z) ^ 2 / (4 * A)
 102
 103noncomputable def binding_per_nucleon (coeff : BindingCoefficients) (A Z : ℕ) : ℝ :=
 104  binding_energy coeff A Z / A
 105
 106/-! ## Structural Results
 107
 108The key structural prediction: binding energy per nucleon peaks near
 109A ≈ 56 (iron-56), and magic-number nuclei have enhanced stability
 110(extra binding). -/
 111
 112theorem volume_dominates_surface (coeff : BindingCoefficients) (A : ℕ) (hA : 8 ≤ A) :
 113    coeff.a_V * A > coeff.a_S * (A : ℝ) ^ ((2:ℝ)/3) := by
 114  have hA_pos : (0 : ℝ) < A := by exact_mod_cast Nat.pos_of_ne_zero (by omega)
 115  nlinarith [coeff.h_V_pos, coeff.h_S_pos, hA_pos,
 116             show (A : ℝ) ^ ((2:ℝ)/3) ≤ A from by
 117               exact Real.rpow_le_self_of_one_le_of_le_one_right (by linarith) (by norm_num)]
 118
 119/-! ## Certificate -/
 120
 121structure NuclearBindingCert where
 122  seven_magic : magic_numbers.length = 7
 123  magic_sorted : magic_numbers.Sorted (· < ·)
 124  eight_from_cube : (8 : ℕ) = 2 ^ 3
 125  twenty_from_cube : (20 : ℕ) = 2 ^ 3 + 3 * 2 ^ 2
 126  coefficients_positive : 0 < rs_binding_coefficients.a_V ∧
 127    0 < rs_binding_coefficients.a_S ∧ 0 < rs_binding_coefficients.a_C
 128
 129theorem nuclear_binding_cert_exists : Nonempty NuclearBindingCert :=
 130  ⟨{ seven_magic := magic_numbers_count
 131     magic_sorted := magic_numbers_sorted
 132     eight_from_cube := magic_8_from_cube
 133     twenty_from_cube := magic_20_from_cube