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

weinberg_angle_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)

 197theorem weinberg_angle_in_range : 0 < rs_weinberg_angle_sq ∧ rs_weinberg_angle_sq < 1 := by

proof body

Tactic-mode proof.

 198  unfold rs_weinberg_angle_sq φ
 199  have h5pos : (0 : ℝ) < Real.sqrt 5 := Real.sqrt_pos.mpr (by norm_num)
 200  have h5lt3 : Real.sqrt 5 < 3 := by
 201    have h9 : Real.sqrt 9 = 3 := by
 202      rw [show (9:ℝ) = 3^2 from by norm_num, Real.sqrt_sq (by norm_num)]
 203    have h : Real.sqrt 5 < Real.sqrt 9 := Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
 204    linarith [h9 ▸ h]
 205  constructor
 206  · apply div_pos _ (by norm_num)
 207    linarith
 208  · rw [div_lt_one (by norm_num)]
 209    linarith
 210
 211/-! ## Gauge Coupling Unification -/
 212
 213/-- At unification scale μ_GUT, the three SM couplings converge.
 214    The RS prediction: μ_GUT lies on the φ-ladder at some integer rung. -/

depends on (10)

Lean names referenced from this declaration's body.