`weak_coupling_approx`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.ElectroweakBosons
domain: Physics
line: 102 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.ElectroweakBosons on GitHub at line 102.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

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]

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.