mW_sq_le_mZ_sq
plain-language theorem explainer
The squared mass of the W boson does not exceed that of the Z boson for any real gauge couplings g, g' and scale v. Electroweak model builders cite this result when confirming the tree-level mass hierarchy in the Standard Model. The argument expands the explicit quadratic forms for the masses and invokes nonnegativity of squares to apply a linear arithmetic solver.
Claim. For all real numbers $g, g', v$, $m_W^2(g, v) = g^2 v^2 / 4$ satisfies $m_W^2(g, v) ≤ m_Z^2(g, g', v)$ where $m_Z^2(g, g', v) = (g^2 + {g'}^2) v^2 / 4$.
background
The Electroweak Mass Bridge module derives Standard Model gauge-boson mass relations from the recognition-substrate scale v together with arbitrary positive gauge couplings g and g'. It formalizes the tree-level expressions m_W² = g² v² / 4 and m_Z² = (g² + g'²) v² / 4, together with the Weinberg-angle identities m_W / m_Z = cos θ_W and sin² θ_W = g'² / (g² + g'²). These relations hold conditionally on the same v supplied by the Higgs EFT bridge; numerical identification of g and g' with measured values remains a separate empirical step. Upstream results supply the present tick from time emergence and anchor maps for W and Z sectors, though the inequality itself rests only on algebraic nonnegativity.
proof idea
The proof unfolds the definitions of the squared-mass expressions. It records nonnegativity of g' squared, v squared, and their product via sq_nonneg and mul_nonneg. It then applies nlinarith to obtain the desired comparison.
why it matters
This theorem supplies the mW_le_mZ field inside electroweakMassBridgeCert and is invoked directly by the companion statement mZ_sq_ge_mW_sq. It completes the unconditional gauge-mass relations inside the Standard Model module, enabling any definition of θ_W (RS or PDG) to be inserted downstream. The result touches the open calibration of g and g' from the recognition substrate, which is tracked separately from the φ-ladder match for v.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.