def
definition
wZRatio
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 83.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
80/-- The W/Z mass ratio:
81 m_W / m_Z = cos θ_W
82 where θ_W is the Weinberg angle. -/
83noncomputable def wZRatio (theta_W : ℝ) : ℝ := Real.cos theta_W
84
85/-- Observed masses:
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? -/