pith. machine review for the scientific record. sign in
theorem proved tactic proof

mH_rs_level2_in_range

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  86theorem mH_rs_level2_in_range : 110 < mH_rs_level2 ∧ mH_rs_level2 < 125 := by

proof body

Tactic-mode proof.

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.