mH_rs_level3_pos

formal source

 114  exact mul_pos sin2ThetaW_RS_pos (by norm_num)
 115
 116/-- mH_rs_level3 is positive. -/
 117theorem mH_rs_level3_pos : 0 < mH_rs_level3 := by
 118  unfold mH_rs_level3 vev
 119  exact mul_pos (by norm_num) (Real.sqrt_pos.mpr q3_correction_pos)
 120
 121/-- **KEY THEOREM**: The RS Higgs mass prediction is in (120, 130) GeV.
 122
 123    This contains the observed value 125.2 GeV and establishes the prediction
 124    as a HYPOTHESIS (not yet THEOREM since the full one-loop EW correction
 125    is not yet formalized). -/
 126theorem mH_prediction_in_interval : 120 < mH_rs_level3 ∧ mH_rs_level3 < 130 := by
 127  unfold mH_rs_level3 vev sin2ThetaW_RS
 128  have hprod_lo : (0.238 : ℝ) < (3 - phi) / 6 * (17 / 16) := by
 129    nlinarith [phi_lt_onePointSixTwo]
 130  have hprod_hi : (3 - phi) / 6 * (17 / 16) < (0.248 : ℝ) := by
 131    nlinarith [phi_gt_onePointSixOne]
 132  constructor
 133  · -- 120 < 246 * √(s2 * 17/16): since (120/246)^2 < 0.238 < s2 * 17/16
 134    have h1 : (120 / 246 : ℝ)^2 < (3 - phi) / 6 * (17 / 16) := by
 135      have : (120 / 246 : ℝ)^2 < 0.238 := by norm_num
 136      linarith
 137    have h2 : (120 / 246 : ℝ) < Real.sqrt ((3 - phi) / 6 * (17 / 16)) := by
 138      rw [← Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 120/246)]
 139      exact Real.sqrt_lt_sqrt (by norm_num) h1
 140    have h3 := mul_lt_mul_of_pos_left h2 (by norm_num : (0:ℝ) < 246)
 141    linarith [show (246:ℝ) * (120/246) = 120 from by ring]
 142  · -- 246 * √(s2 * 17/16) < 130: since s2 * 17/16 < 0.248 < (130/246)^2
 143    have h1 : (3 - phi) / 6 * (17 / 16) < (130 / 246 : ℝ)^2 := by
 144      have : (130 / 246 : ℝ)^2 > 0.278 := by norm_num
 145      linarith
 146    have h2 : Real.sqrt ((3 - phi) / 6 * (17 / 16)) < 130 / 246 := by
 147      rw [← Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 130/246)]