volume_dominates_surface

formal source

 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
 134     coefficients_positive := ⟨rs_binding_coefficients.h_V_pos,
 135       rs_binding_coefficients.h_S_pos, rs_binding_coefficients.h_C_pos⟩ }⟩
 136
 137end
 138
 139end IndisputableMonolith.Nuclear.BindingEnergy