wBosonMass

formal source

  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
  90noncomputable def mZ_observed : ℝ := 91.2
  91
  92/-! ## J-Cost Interpretation -/
  93
  94/-- In RS, the Higgs potential is a J-cost functional:
  95
  96    J(φ) = J_kinetic(φ) + J_potential(φ)
  97
  98    J_potential = -μ²|φ|² + λ|φ|⁴
  99
 100    This is exactly the Higgs potential! -/
 101noncomputable def jcostHiggs (phi mu_sq lambda : ℝ) : ℝ :=
 102  Jcost (-mu_sq * phi^2 + lambda * phi^4)
 103