def
definition
summary
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.StandardModel.ElectroweakBreaking on GitHub at line 248.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
245 4. **Photon massless**: U(1)_EM unbroken
246 5. **Higgs boson**: Radial excitation of Higgs field
247 6. **Hierarchy**: May be φ-related (under investigation) -/
248def summary : List String := [
249 "Higgs potential = J-cost functional",
250 "VEV = J-cost minimum",
251 "W, Z get mass, photon stays massless",
252 "Higgs boson discovered at 125 GeV",
253 "Hierarchy problem: v << M_Planck"
254]
255
256/-! ## Falsification Criteria -/
257
258/-- The derivation would be falsified if:
259 1. Higgs mechanism is wrong
260 2. VEV doesn't minimize J-cost
261 3. Additional Higgs bosons found (complicates story) -/
262structure ElectroweakBreakingFalsifier where
263 higgs_wrong : Prop
264 vev_not_minimum : Prop
265 extra_higgs : Prop
266 falsified : higgs_wrong ∨ vev_not_minimum → False
267
268end ElectroweakBreaking
269end StandardModel
270end IndisputableMonolith