def
definition
phiCorrection
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.StandardModel.WeinbergAngle on GitHub at line 144.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
141 This gives: 0.25 × (1 - 0.032) = 0.242 × 0.968 = 0.234
142
143 Still a bit too large, but capturing the right structure. -/
144noncomputable def phiCorrection : ℝ := (phi - 1) / (12 * phi)
145
146noncomputable def correctedPrediction : ℝ := (1/4) * (1 - phiCorrection)
147
148/-! ## Grand Unified Theory Connection -/
149
150/-- At the GUT scale (~10¹⁶ GeV), the couplings unify.
151
152 sin²(θ_W)(GUT) = 3/8 = 0.375 (SU(5) prediction)
153
154 The running from GUT to M_Z scale is:
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: