`alpha_s_err`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.StrongForce
domain: Physics
line: 39 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.StrongForce on GitHub at line 39.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  36/-! ## Experimental Value -/
  37
  38def alpha_s_exp : ℝ := 0.1179
  39def alpha_s_err : ℝ := 0.0009
  40
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.