theorem
proved
photon_massless
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.StandardModel.ElectroweakBreaking on GitHub at line 203.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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"
227
228/-- Higgs couplings:
229
230 H couples to mass:
231 - g_Hff = m_f / v (fermions)
232 - g_HVV = 2 m_V² / v (gauge bosons)
233