def
definition
vev_observed
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.StandardModel.ElectroweakBreaking on GitHub at line 59.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
56 Real.sqrt (mu_sq / (2 * lambda))
57
58/-- The observed VEV is v ≈ 246 GeV. -/
59noncomputable def vev_observed : ℝ := 246 -- GeV
60
61/-- The Higgs mass is determined by the curvature at the minimum. -/
62noncomputable def higgsMass (lambda : ℝ) (v : ℝ) : ℝ :=
63 Real.sqrt (2 * lambda) * v
64
65/-- The observed Higgs mass is m_H ≈ 125 GeV. -/
66noncomputable def higgsMass_observed : ℝ := 125 -- GeV
67
68/-! ## Mass Generation -/
69
70/-- W boson mass from Higgs VEV:
71 m_W = g v / 2
72 where g is the SU(2) coupling. -/
73noncomputable def wBosonMass (g v : ℝ) : ℝ := g * v / 2
74
75/-- Z boson mass from Higgs VEV:
76 m_Z = v √(g² + g'²) / 2
77 where g' is the U(1) coupling. -/
78noncomputable def zBosonMass (g g' v : ℝ) : ℝ := v * Real.sqrt (g^2 + g'^2) / 2
79
80/-- The W/Z mass ratio:
81 m_W / m_Z = cos θ_W
82 where θ_W is the Weinberg angle. -/
83noncomputable def wZRatio (theta_W : ℝ) : ℝ := Real.cos theta_W
84
85/-- Observed masses:
86 m_W ≈ 80.4 GeV
87 m_Z ≈ 91.2 GeV
88 Ratio ≈ 0.882 -/
89noncomputable def mW_observed : ℝ := 80.4