$m_Z = m_W/\cos\theta_W$

Proved

ElectroweakWiki.zMass_eq_wMass_div_cos

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

electroweakmathematical-physics

Let $g>0$ , $g'>0$ , $v\in\mathbb R$ , $\theta_W = \arctan(g'/g)$ , and let $m_W = gv/2$ and $m_Z = \sqrt{g^2+g'^2}\,v/2$ be the tree-level masses. Then

m_Z = \frac{m_W}{\cos\theta_W}.

This is the mass relation between the $Z^0$ and the $W^\pm$ quoted in the article.

Preamble

import Definitions.Def_ElectroweakWiki_defs
open Matrix

Formal statement

namespace ElectroweakWiki

theorem zMass_eq_wMass_div_cos (g g' v : ℝ) (hg : 0 < g) (hg' : 0 < g') :
    zMass g g' v = wMass g v / Real.cos (weinbergAngle g g') := by sorry

end ElectroweakWiki

Source

Wikipedia, "Electroweak interaction", revision oldid=1360331872, https://en.wikipedia.org/w/index.php?title=Electroweak_interaction&oldid=1360331872; Section Formulation, 'This also introduces a mismatch between the mass of the Z0 and the mass of the W± particles: mZ = mW / cos θW' (p. 3 of the PDF)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted these Lean statements (at the explicit direction of the proposal's owner), not by an independent blind auditor. The author knew the intended meaning while writing it, so it must not be mistaken for independent testimony; reviewers should check it against the Lean code themselves.

For all real $g, g', v$ with $g>0$ and $g'>0$ , with $\theta = \arctan(g'/g)$ , the statement asserts

\frac{\sqrt{g^2+g'^2}\,v}{2} = \frac{gv/2}{\cos\theta}.

No sign condition is placed on $v$ .

View graph

mZ=mW/cos⁡θWm_Z = m_W/\cos\theta_WmZ​=mW​/cosθW​

$m_Z = m_W/\cos\theta_W$