weak_coupling_approx

formal source

  99def weak_coupling_g : ℝ := 2 * wBosonMass_GeV / vev_GeV
 100
 101/-- g ≈ 0.653 (weak coupling constant). -/
 102theorem weak_coupling_approx : |weak_coupling_g - 0.653| < 0.01 := by
 103  -- 2 × 80.3692 / 246.22 = 160.7384 / 246.22 ≈ 0.6528
 104  -- |0.6528 - 0.653| = 0.0002 < 0.01
 105  simp only [weak_coupling_g, wBosonMass_GeV, vev_GeV]
 106  norm_num
 107
 108/-! ## Key Theorems -/
 109
 110/-- W boson mass is approximately 80 GeV. -/
 111theorem w_mass_near_80 : |wBosonMass_GeV - 80| < 1 := by
 112  simp only [wBosonMass_GeV]
 113  norm_num
 114
 115/-- Z boson mass is approximately 91 GeV. -/
 116theorem z_mass_near_91 : |zBosonMass_GeV - 91| < 1 := by
 117  simp only [zBosonMass_GeV]
 118  norm_num
 119
 120/-- Z is heavier than W. -/
 121theorem z_heavier_than_w : zBosonMass_GeV > wBosonMass_GeV := by
 122  simp only [zBosonMass_GeV, wBosonMass_GeV]
 123  norm_num
 124
 125/-- Both electroweak gauge-boson masses are strictly positive. -/
 126theorem wz_masses_positive : 0 < wBosonMass_GeV ∧ 0 < zBosonMass_GeV := by
 127  have hw := w_mass_near_80
 128  have hz := z_mass_near_91
 129  rw [abs_lt] at hw hz
 130  constructor
 131  · linarith [hw.1]
 132  · linarith [hz.1]