m_W_exp
plain-language theorem explainer
The declaration supplies the experimental W-boson mass 80369.2 as a fixed real constant inside the ElectroweakMasses module. Researchers comparing RS-derived m_W = m_Z cos θ_W against data cite this value for ratio checks. It is introduced by direct numerical assignment with no derivation or proof steps.
Claim. The experimental W-boson mass is the real number $m_W^exp = 80369.2$ (MeV).
background
The ElectroweakMasses module differentiates boson masses from the earlier r_boson placeholder. The Z boson sits at rung 1, so m_Z = 2 φ^51 / 10^6 MeV. The W mass is obtained from the gauge relation m_W = m_Z cos θ_W, where sin²θ_W = (3 − φ)/6 supplies the zero-parameter RS value for the Weinberg angle. This definition supplies the measured benchmark used for direct numerical comparison.
proof idea
One-line definition that directly assigns the constant 80369.2 to m_W_exp.
why it matters
It supplies the experimental input for the downstream wz_ratio_exp_comparison theorem, which checks that (m_W_exp / m_Z_exp)^2 lies in (0.7765, 0.7775). The definition therefore closes the verification loop between the RS prediction m_W = m_Z cos θ_W and measured data inside the electroweak sector of the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.