mH_rs_level3

formal source

 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. -/
 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