sin2_theta_window

formal source

 141  norm_num
 142
 143/-- Observed weak-mixing value lies in the physical interval `(0,1)`. -/
 144theorem sin2_theta_window : 0 < sin2_theta_W ∧ sin2_theta_W < 1 := by
 145  have hs := sin2_theta_approx
 146  rw [abs_lt] at hs
 147  constructor
 148  · linarith [hs.1]
 149  · linarith [hs.2]
 150
 151/-- Observed weak-mixing value excludes the maximal-mixing midpoint `1/2`. -/
 152theorem sin2_theta_not_half : sin2_theta_W ≠ (1 / 2 : ℝ) := by
 153  have hs := sin2_theta_approx
 154  rw [abs_lt] at hs
 155  linarith [hs.2]
 156
 157/-- Observed W/Z mass ratio is strictly below unity. -/
 158theorem wz_ratio_lt_one : wz_mass_ratio < 1 := by
 159  unfold wz_mass_ratio wBosonMass_GeV zBosonMass_GeV
 160  norm_num
 161
 162/-! ## φ-Ladder Connection -/
 163
 164/-- Electron mass in GeV. -/
 165def electronMass_GeV : ℝ := 0.000511
 166
 167/-- W to electron mass ratio. -/
 168def w_electron_ratio : ℝ := wBosonMass_GeV / electronMass_GeV
 169
 170/-- φ^23 is close to the W/e mass ratio scale. -/
 171def phi_23 : ℝ := phi ^ 23
 172
 173/-- φ^24 is close to the Z/e mass ratio scale. -/
 174def phi_24 : ℝ := phi ^ 24