mZ_sq_ge_mW_sq
plain-language theorem explainer
The theorem shows that the squared mass of the Z boson is at least as large as the squared mass of the W boson for arbitrary real gauge couplings g, g' and scale v. Researchers checking tree-level electroweak relations or embedding the Standard Model into a larger framework would cite this when confirming the ordering of gauge-boson masses. The proof is a direct one-line application of the sibling inequality that already encodes the non-negative contribution of g'^2.
Claim. For all real numbers $g, g', v$, the squared W-boson mass satisfies $m_W^2(g, v) = g^2 v^2 / 4$ and the squared Z-boson mass satisfies $m_Z^2(g, g', v) = (g^2 + g'^2) v^2 / 4$, so $m_W^2(g, v) ≤ m_Z^2(g, g', v)$.
background
The Electroweak Mass Bridge module supplies the tree-level gauge-boson mass relations that follow once a common recognition-substrate scale $v$ and arbitrary real couplings $g, g'$ are given. Explicitly, $m_W^2 = g^2 v^2 / 4$ and $m_Z^2 = (g^2 + g'^2) v^2 / 4$, which immediately imply the Weinberg-angle identities $m_W / m_Z = g / √(g^2 + g'^2)$ and $sin^2 θ_W = g'^2 / (g^2 + g'^2)$. These relations are conditional on the same $v$ supplied by the Higgs EFT bridge; they do not yet fix the numerical values of $g$ and $g'$. Upstream results supply the definitions of the squared-mass functions $mW_sq$ and $mZ_sq$ together with the non-negativity of $g'^2$ for real $g'$.
proof idea
The proof is a one-line wrapper that applies the sibling lemma mW_sq_le_mZ_sq g gp v, which already encodes the algebraic comparison $g^2 ≤ g^2 + g'^2$. No further tactics or case splits are required.
why it matters
The result completes the basic ordering of gauge-boson masses inside the Electroweak Mass Bridge, thereby supporting all subsequent tree-level SM identities derived in the same module. It sits downstream of the recognition-substrate scale $v$ and upstream of any numerical calibration of $g, g'$ against the phi-ladder mass formula. Because the module treats the identification of $g, g'$ with measured values as an open empirical step, this inequality remains available for any choice of positive couplings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.