def
definition
def or abbrev
correctedPrediction
show as:
view Lean formalization →
formal statement (Lean)
146noncomputable def correctedPrediction : ℝ := (1/4) * (1 - phiCorrection)
proof body
Definition body.
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! -/