alpha_s_geom

formal source

  41/-! ## Theoretical Prediction -/
  42
  43/-- The Wallpaper Fraction: 2/17. -/
  44def alpha_s_geom : ℚ := 2 / 17
  45
  46/-- Predicted Strong Coupling. -/
  47noncomputable def alpha_s_pred : ℝ := alpha_s_geom
  48
  49/-! ## Geometric Derivation -/
  50
  51/-- The prediction derives from wallpaper group count. -/
  52theorem alpha_s_pred_eq_two_over_W :
  53    alpha_s_pred = 2 / (wallpaper_groups : ℝ) := by
  54  simp only [alpha_s_pred, alpha_s_geom, wallpaper_groups]
  55  norm_num
  56
  57/-- Exact value of 2/17 as real. -/
  58theorem alpha_s_geom_eq : (alpha_s_geom : ℝ) = 2 / 17 := by
  59  simp only [alpha_s_geom]
  60  norm_num
  61
  62/-! ## Verification -/
  63
  64/-- Helper: 2/17 bounds using direct computation. -/
  65theorem two_div_17_lower : (0.117 : ℝ) < (alpha_s_geom : ℝ) := by
  66  simp only [alpha_s_geom]
  67  norm_num
  68
  69theorem two_div_17_upper : (alpha_s_geom : ℝ) < 0.118 := by
  70  simp only [alpha_s_geom]
  71  norm_num
  72
  73/-- The predicted value is within experimental error of the measured value.
  74