alpha_seed

formal source

  92/-! ## The Three Ingredients -/
  93
  94/-- Geometric seed: 4π × passive_edges. -/
  95def alpha_seed : ℝ := 4 * π * passive_edges
  96
  97/-- Gap weight (from DFT-8 projection — see Constants.GapWeight). -/
  98def f_gap (w8 : ℝ) : ℝ := w8 * Real.log φ where
  99  φ := (1 + Real.sqrt 5) / 2
 100
 101/-- First-order curvature correction. -/
 102def delta_1 : ℝ := -(curvature_numerator : ℝ) / ((face_wallpaper_pairs : ℝ) * π ^ measure_dimension)
 103
 104theorem delta_1_structure :
 105    delta_1 = -(curvature_numerator : ℝ) / ((face_wallpaper_pairs : ℝ) * π ^ measure_dimension) :=
 106  rfl
 107
 108theorem delta_1_numerator : (curvature_numerator : ℕ) = 103 := curvature_numerator_eq
 109theorem delta_1_denominator_nat : (face_wallpaper_pairs : ℕ) = 102 := face_wallpaper_pairs_eq
 110theorem delta_1_power : measure_dimension = 5 := measure_dimension_eq
 111
 112/-- δ₁ is negative (the curvature correction subtracts). -/
 113theorem delta_1_neg : delta_1 < 0 := by
 114  unfold delta_1
 115  have hnum : (0 : ℝ) < (curvature_numerator : ℝ) := by
 116    simp [curvature_numerator, face_wallpaper_pairs, Q3_faces, wallpaper_groups, active_edges]
 117  have hfwp : (0 : ℝ) < (face_wallpaper_pairs : ℝ) := by
 118    simp [face_wallpaper_pairs, Q3_faces, wallpaper_groups]
 119  have hden : (0 : ℝ) < (face_wallpaper_pairs : ℝ) * π ^ measure_dimension :=
 120    mul_pos hfwp (pow_pos pi_pos _)
 121  exact div_neg_of_neg_of_pos (neg_neg_of_pos hnum) hden
 122
 123/-! ## n-fold Configuration Space -/
 124
 125/-- The number of ordered n-fold face-wallpaper configurations. -/