higgsPotential

formal source

  48/-! ## The Higgs Potential -/
  49
  50/-- The Higgs potential in the Standard Model. -/
  51noncomputable def higgsPotential (phi mu_sq lambda : ℝ) : ℝ :=
  52  -mu_sq * phi^2 + lambda * phi^4
  53
  54/-- The VEV (vacuum expectation value) of the Higgs field. -/
  55noncomputable def vev (mu_sq lambda : ℝ) (_h_mu : mu_sq > 0) (_h_lambda : lambda > 0) : ℝ :=
  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