mH_obs

formal source

  66noncomputable def mZ_obs : ℝ := 91.2
  67
  68/-- Higgs observed mass in GeV. -/
  69noncomputable def mH_obs : ℝ := 125.2
  70
  71/-- The VEV is positive. -/
  72theorem vev_pos : 0 < vev := by unfold vev; norm_num
  73
  74/-! ## RS Higgs Mass Prediction -/
  75
  76/-- Level 1: "Naive" RS prediction from m_H = v.
  77    This follows from λ_RS = 1/2, m_H² = 2λv² = v². -/
  78noncomputable def mH_naive : ℝ := vev
  79
  80/-- Level 2: RS prediction with sin²θ_W correction.
  81    m_H = v · √(sin²θ_W) — the dominant correction from Q₃ symmetry breaking. -/
  82noncomputable def mH_rs_level2 : ℝ :=
  83  vev * Real.sqrt sin2ThetaW_RS
  84
  85/-- mH_rs_level2 is in (110, 125). -/
  86theorem mH_rs_level2_in_range : 110 < mH_rs_level2 ∧ mH_rs_level2 < 125 := by
  87  unfold mH_rs_level2 vev sin2ThetaW_RS
  88  have hs2_lo : (0.228 : ℝ) < (3 - phi) / 6 := by linarith [phi_lt_onePointSixTwo]
  89  have hs2_hi : (3 - phi) / 6 < (0.233 : ℝ) := by linarith [phi_gt_onePointSixOne]
  90  have hs2_pos : (0 : ℝ) < (3 - phi) / 6 := by linarith
  91  constructor
  92  · -- 110 < 246 * √s2: since (110/246)^2 ≈ 0.2 < 0.228 < s2
  93    have h1 : (110 / 246 : ℝ)^2 < (3 - phi) / 6 := by nlinarith
  94    have h2 : (110 / 246 : ℝ) < Real.sqrt ((3 - phi) / 6) := by
  95      rw [← Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 110/246)]
  96      exact Real.sqrt_lt_sqrt (by norm_num) h1
  97    linarith [mul_lt_mul_of_pos_left h2 (by norm_num : (0:ℝ) < 246)]
  98  · -- 246 * √s2 < 125: since s2 < 0.233 < (125/246)^2 ≈ 0.258
  99    have h1 : (3 - phi) / 6 < (125 / 246 : ℝ)^2 := by nlinarith