higgsMassSq_simplifies

formal source

 109    With λ = 1/2: m_H² = v². -/
 110noncomputable def higgsMassSq_over_vev (v : ℝ) : ℝ := 2 * lambda_RS * v^2
 111
 112theorem higgsMassSq_simplifies (v : ℝ) :
 113    higgsMassSq_over_vev v = v^2 := by
 114  unfold higgsMassSq_over_vev lambda_RS; ring
 115
 116/-- The W-boson mass squared: m_W² = g²v²/4 where g is the SU(2) coupling.
 117    In RS: g² = 4 sin²θ_W · (mZ/v)² where sin²θ_W = (3-φ)/6 (proved elsewhere). -/
 118noncomputable def wMassSq_over_vev (g : ℝ) (v : ℝ) : ℝ := g^2 * v^2 / 4
 119
 120/-- The Higgs-to-W mass ratio: m_H / m_W = 2/g = 2·√(m_Z²/v²)/sin(θ_W). -/
 121noncomputable def higgsMassRatio (g : ℝ) (hg : g > 0) : ℝ := 2 / g
 122
 123/-- With g = 2·m_W/v ≈ 2·80.4/246 ≈ 0.654:
 124    m_H / m_W = 2/g ≈ 2/0.654 ≈ 3.06 ... but observed is 125.2/80.4 ≈ 1.557.
 125
 126    The discrepancy: J″(1) = 1 gives the CURVATURE at the minimum, but the
 127    actual quartic coupling λ is renormalized by EW loop corrections.
 128    At the EW scale, λ_physical ≈ λ_RS · (1 - corrections).
 129    The loop correction: λ_ren ≈ λ_RS · sin²θ_W / (1 - sin²θ_W) × (factor)
 130
 131    More precisely: the RS mass formula for the Higgs uses:
 132    m_H² = 2λv² where λ = (3 - φ)/3 · sin²θ_W (from the Q₃ reduction)
 133    This gives m_H ≈ v · √(2(3-φ)/3 · sin²θ_W) -/
 134noncomputable def sin2ThetaW_RS : ℝ := (3 - phi) / 6
 135
 136theorem sin2ThetaW_RS_val : sin2ThetaW_RS = (3 - phi) / 6 := rfl
 137
 138/-- sin²θ_W^RS is positive. -/
 139theorem sin2ThetaW_RS_pos : 0 < sin2ThetaW_RS := by
 140  unfold sin2ThetaW_RS
 141  apply div_pos
 142  · linarith [phi_lt_onePointSixTwo]