two_is_magic

formal source

  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)
  75  a_S : ℝ  -- surface (MeV)
  76  a_C : ℝ  -- Coulomb (MeV)
  77  a_A : ℝ  -- asymmetry (MeV)
  78  a_P : ℝ  -- pairing (MeV)
  79  h_V_pos : 0 < a_V
  80  h_S_pos : 0 < a_S