def
definition
sin2ThetaW_GUT
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.StandardModel.WeinbergAngle on GitHub at line 158.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
155 sin²(θ_W)(M_Z) ≈ 0.23
156
157 RS explains both the GUT value AND the running! -/
158noncomputable def sin2ThetaW_GUT : ℝ := 3/8
159
160/-- **THEOREM**: GUT value is 3/8. -/
161theorem gut_prediction : sin2ThetaW_GUT = 3/8 := rfl
162
163/-- The running of sin²(θ_W) with energy follows the φ-ladder.
164
165 At energy E:
166 sin²(θ_W)(E) = sin²(θ_W)(GUT) × (1 - α log(E/E_GUT))
167
168 where α involves φ. -/
169noncomputable def runningAngle (logEnergy : ℝ) : ℝ :=
170 sin2ThetaW_GUT * (1 - logEnergy / (16 * Real.pi^2))
171
172/-! ## The Deep Connection -/
173
174/-- The Weinberg angle encodes fundamental information:
175
176 1. **Charge quantization**: Q = I₃ + Y/2, where I₃ and Y mix by θ_W
177 2. **Mass relations**: m_W = m_Z × cos(θ_W)
178 3. **Coupling unification**: At high energy, couplings merge
179
180 In RS, all three emerge from the 8-tick structure with φ-optimization. -/
181def deepConnections : List String := [
182 "Charge quantization from discrete phases",
183 "Mass ratio from φ-constrained symmetry breaking",
184 "Unification from φ-ladder convergence"
185]
186
187/-! ## Experimental Tests -/
188