theorem
proved
alpha_s_value
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Unification.GaugeCouplingsComplete on GitHub at line 137.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
134/-! ## C-014: Numerical Predictions -/
135
136/-- **CALCULATED**: α_s = 2/17 ≈ 0.117647... -/
137theorem alpha_s_value : (0.117 : ℝ) < (alpha_s_pred : ℝ) ∧ (alpha_s_pred : ℝ) < (0.118 : ℝ) := by
138 constructor
139 · -- Lower bound: 2/17 > 0.117
140 simp only [alpha_s_pred, alpha_s_geom]
141 norm_num
142 · -- Upper bound: 2/17 < 0.118
143 simp only [alpha_s_pred, alpha_s_geom]
144 norm_num
145
146/-- **CALCULATED**: sin²θ_w from φ ≈ 0.230 (matches observed 0.2229 within ~3%) -/
147theorem weak_mixing_bounds :
148 (0.22 : ℝ) < bestPrediction ∧ bestPrediction < (0.24 : ℝ) := by
149 unfold bestPrediction prediction3
150 have h1 : phi > 1.61 := phi_gt_onePointSixOne
151 have h2 : phi < 1.62 := phi_lt_onePointSixTwo
152 constructor
153 · -- (3 - φ)/6 > (3 - 1.62)/6 = 1.38/6 = 0.23
154 have h3 : (3 - phi) / 6 > (0.22 : ℝ) := by
155 linarith
156 linarith
157 · -- (3 - φ)/6 < (3 - 1.61)/6 = 1.39/6 = 0.2317
158 have h4 : (3 - phi) / 6 < (0.24 : ℝ) := by
159 linarith
160 linarith
161
162/-- **BOUNDS**: α_s is within experimental error of PDG value. -/
163theorem alpha_s_within_pdg_bounds : abs (alpha_s_pred - 0.1179) < 0.0009 :=
164 alpha_s_match
165
166/-! ## C-014: Gauge Unification -/
167