magic_numbers

formal source

  41
  42/-! ## Nuclear Magic Numbers -/
  43
  44def magic_numbers : List ℕ := [2, 8, 20, 28, 50, 82, 126]
  45
  46theorem magic_numbers_count : magic_numbers.length = 7 := by decide
  47
  48theorem magic_numbers_sorted : magic_numbers.Sorted (· < ·) := by decide
  49
  50theorem two_is_magic : 2 ∈ magic_numbers := by decide
  51theorem eight_is_magic : 8 ∈ magic_numbers := by decide
  52theorem twenty_is_magic : 20 ∈ magic_numbers := by decide
  53theorem twentyeight_is_magic : 28 ∈ magic_numbers := by decide
  54
  55/-! ## 8-Tick Connection
  56
  57The first magic numbers connect directly to D=3 cube geometry:
  58- 2 = number of vertices per edge of Q₃
  59- 8 = 2^D = number of vertices of Q₃ (one full tick cycle)
  60- 12 = number of edges of Q₃
  61- 20 = 8 + 12 (vertices + edges) -/
  62
  63theorem magic_2_from_dimension : (2 : ℕ) = 2 ^ 1 := by norm_num
  64theorem magic_8_from_cube : (8 : ℕ) = 2 ^ 3 := by norm_num
  65theorem magic_20_from_cube : (20 : ℕ) = 2 ^ 3 + 3 * 2 ^ 2 := by norm_num
  66theorem magic_28_from_cube : (28 : ℕ) = 2 ^ 3 + 3 * 2 ^ 2 + 2 ^ 3 := by norm_num
  67
  68/-! ## Weizsacker-like Binding Energy Formula
  69
  70The semi-empirical mass formula with RS-motivated structure.
  71All coefficients are functions of φ and the 8-tick geometry. -/
  72
  73structure BindingCoefficients where
  74  a_V : ℝ  -- volume (MeV)