`rs_hierarchy`

proved

show as: view math explainer →

module: IndisputableMonolith.StandardModel.ElectroweakBreaking
domain: StandardModel
line: 179 · 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 179.

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

 176    Need φ⁸⁰ ≈ 10¹⁶... hmm.
 177
 178    Note: The exact φ-relationship is still under investigation. -/
 179theorem rs_hierarchy :
 180    -- Basic fact: v << M_Planck (about 10^17 ratio)
 181    -- We prove the ratio is indeed very large
 182    let M_Planck : ℝ := 1.22e19  -- GeV
 183    vev_observed / M_Planck < 1e-15 := by
 184  unfold vev_observed
 185  norm_num
 186
 187/-! ## Goldstone Bosons -/
 188
 189/-- When symmetry breaks, Goldstone bosons appear:
 190
 191    SU(2)_L × U(1)_Y → U(1)_EM
 192
 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

papers checked against this theorem

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