mH_rs_level2_in_range

formal source

  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
 100    have h2 : Real.sqrt ((3 - phi) / 6) < 125 / 246 := by
 101      rw [← Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 125/246)]
 102      exact Real.sqrt_lt_sqrt (by linarith) h1
 103    linarith [mul_lt_mul_of_pos_left h2 (by norm_num : (0:ℝ) < 246)]
 104
 105/-- Level 3: RS prediction with Q₃ 1/16 correction factor.
 106    m_H = v · √(sin²θ_W · 17/16)
 107    The factor 17/16 = 1 + 1/16 comes from the Q₃ mode budget:
 108    16 addressing modes total, 17th = the physical Higgs singlet mode. -/
 109noncomputable def mH_rs_level3 : ℝ :=
 110  vev * Real.sqrt (sin2ThetaW_RS * (17 / 16))
 111
 112/-- The Q₃ correction factor 17/16 is positive. -/
 113theorem q3_correction_pos : 0 < sin2ThetaW_RS * (17 / 16 : ℝ) := by
 114  exact mul_pos sin2ThetaW_RS_pos (by norm_num)
 115
 116/-- mH_rs_level3 is positive. -/