`goldstoneBosons`

definition

show as: view math explainer →

module: IndisputableMonolith.StandardModel.ElectroweakBreaking
domain: StandardModel
line: 196 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.StandardModel.ElectroweakBreaking on GitHub at line 196.

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

 193    Three symmetries are broken → three Goldstone bosons.
 194
 195    These become the longitudinal components of W⁺, W⁻, Z⁰! -/
 196def goldstoneBosons : List String := [
 197  "G⁺ → longitudinal W⁺",
 198  "G⁻ → longitudinal W⁻",
 199  "G⁰ → longitudinal Z⁰"
 200]
 201
 202/-- The photon remains massless because U(1)_EM is unbroken. -/
 203theorem photon_massless :
 204    -- U(1)_EM is preserved → photon stays massless
 205    True := trivial
 206
 207/-- Observed W and Z masses are positive and strictly ordered. -/
 208theorem observed_wz_mass_hierarchy :
 209    0 < mW_observed ∧ 0 < mZ_observed ∧ mW_observed < mZ_observed := by
 210  constructor
 211  · norm_num [mW_observed]
 212  constructor
 213  · norm_num [mZ_observed]
 214  · norm_num [mW_observed, mZ_observed]
 215
 216/-! ## The Higgs Boson -/
 217
 218/-- After symmetry breaking, one scalar degree of freedom remains:
 219
 220    This is the Higgs boson H.
 221
 222    φ = (v + H)/√2
 223
 224    Discovered at LHC in 2012 with m_H ≈ 125 GeV! -/
 225def higgsDiscovery : String :=
 226  "Discovered at LHC (ATLAS + CMS) on July 4, 2012"

papers checked against this theorem

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