weinberg_angle_in_range

formal source

 194noncomputable def rs_weinberg_angle_sq : ℝ := (3 - φ) / 6
 195
 196/-- Weinberg angle is between 0 and 1. -/
 197theorem weinberg_angle_in_range : 0 < rs_weinberg_angle_sq ∧ rs_weinberg_angle_sq < 1 := by
 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. -/
 215structure GUTUnification where
 216  μ_GUT : ℝ  -- unification scale in GeV
 217  rung : ℤ   -- φ-ladder rung: μ_GUT = E_coh × φ^rung
 218  h_pos : 0 < μ_GUT
 219
 220/-- The GUT scale is above the electroweak scale. -/
 221theorem gut_above_ew (gut : GUTUnification) :
 222    rs_anchor_scale < gut.μ_GUT → 0 < gut.μ_GUT :=
 223  fun h => by unfold rs_anchor_scale at h; linarith
 224
 225/-! ## QCD Mass Running (Leading Order)
 226
 227The QCD mass anomalous dimension governs how quark masses change with