theorem
proved
alpha_s_geom_eq
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.StrongForce on GitHub at line 58.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
75 pred = 2/17 ≈ 0.117647...
76 exp = 0.1179
77 err = 0.0009
78
79 |pred - exp| = |0.117647 - 0.1179| = 0.000253 < 0.0009 ✓
80
81 This is now PROVEN, not axiomatized. -/
82theorem alpha_s_match :
83 abs (alpha_s_pred - alpha_s_exp) < alpha_s_err := by
84 simp only [alpha_s_pred, alpha_s_geom, alpha_s_exp, alpha_s_err]
85 norm_num
86
87/-! ## Certificate -/
88