vev_determines_scale

formal source

 210/-! ## Electroweak Unification Scale -/
 211
 212/-- The electroweak scale v = 246 GeV sets the mass scale. -/
 213theorem vev_determines_scale :
 214    wBosonMass_GeV < vev_GeV ∧
 215    zBosonMass_GeV < vev_GeV ∧
 216    higgsMass_GeV < vev_GeV * 0.6 := by
 217  simp only [wBosonMass_GeV, zBosonMass_GeV, higgsMass_GeV, vev_GeV]
 218  norm_num
 219
 220/-- The Higgs and electroweak VEV scales are non-degenerate. -/
 221theorem vev_not_equal_higgs_mass : vev_GeV ≠ higgsMass_GeV := by
 222  have hwpos : 0 < wBosonMass_GeV := wz_masses_positive.1
 223  have hscale := vev_determines_scale
 224  have hvev : 0 < vev_GeV := lt_trans hwpos hscale.1
 225  have h06 : (0.6 : ℝ) < 1 := by norm_num
 226  have hmul : vev_GeV * 0.6 < vev_GeV := by
 227    have hmul' : vev_GeV * 0.6 < vev_GeV * 1 := mul_lt_mul_of_pos_left h06 hvev
 228    simpa using hmul'
 229  have hh_lt_vev : higgsMass_GeV < vev_GeV := lt_trans hscale.2.2 hmul
 230  intro hEq
 231  linarith [hh_lt_vev, hEq]
 232
 233/-! ## 8-Tick Connection -/
 234
 235/-- The W, Z, photon, and Higgs form a 4-boson electroweak sector. -/
 236def electroweakBosons : ℕ := 4
 237
 238/-- 8 / 2 = 4 bosons. -/
 239theorem electroweak_8_tick : 8 / 2 = 4 := by native_decide
 240
 241/-- The Z⁰ has 3 polarization states (massive spin-1). -/
 242def zPolarizations : ℕ := 3
 243