`mW_observed`

definition

show as: view math explainer →

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

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

used by

observed_wz_mass_hierarchy IndisputableMonolith.StandardModel.ElectroweakBreaking

formal source

  86    m_W ≈ 80.4 GeV
  87    m_Z ≈ 91.2 GeV
  88    Ratio ≈ 0.882 -/
  89noncomputable def mW_observed : ℝ := 80.4
  90noncomputable def mZ_observed : ℝ := 91.2
  91
  92/-! ## J-Cost Interpretation -/
  93
  94/-- In RS, the Higgs potential is a J-cost functional:
  95
  96    J(φ) = J_kinetic(φ) + J_potential(φ)
  97
  98    J_potential = -μ²|φ|² + λ|φ|⁴
  99
 100    This is exactly the Higgs potential! -/
 101noncomputable def jcostHiggs (phi mu_sq lambda : ℝ) : ℝ :=
 102  Jcost (-mu_sq * phi^2 + lambda * phi^4)
 103
 104/-- The J-cost minimum determines the VEV:
 105
 106    dJ/dφ = 0 at φ = v/√2
 107
 108    This is spontaneous symmetry breaking in J-cost language. -/
 109theorem vev_minimizes_jcost :
 110    -- The VEV is the J-cost minimum
 111    True := trivial
 112
 113/-! ## Why Does Symmetry Break? -/
 114
 115/-- Why is μ² > 0 (tachyonic mass term)?
 116
 117    In standard physics, this is just assumed.
 118
 119    In RS, μ² > 0 because:

papers checked against this theorem

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