mW_sq_lt_mZ_sq_of_gp_pos
plain-language theorem explainer
The theorem shows that the squared W-boson mass is strictly less than the squared Z-boson mass whenever the hypercharge coupling is positive and the vacuum scale is positive. Electroweak phenomenologists cite it to recover the observed m_W < m_Z hierarchy directly from the gauge couplings without further assumptions. The proof unfolds the two quadratic mass expressions, records positivity of the squares via the positivity tactic, and closes the inequality with nlinarith on the resulting positive term.
Claim. For real numbers $g, g', v$ with $g' > 0$ and $v > 0$, $m_W^2(g, v) < m_Z^2(g, g', v)$, where $m_W^2 = g^2 v^2 / 4$ and $m_Z^2 = (g^2 + g'^2) v^2 / 4$.
background
The ElectroweakMassBridge module derives the tree-level Standard Model gauge-boson mass relations from a single positive vacuum scale $v$ supplied by the recognition substrate together with arbitrary positive gauge couplings $g$ and $g'$. The defining relations are $m_W^2 = g^2 v^2 / 4$ and $m_Z^2 = (g^2 + g'^2) v^2 / 4$, which encode the effect of $U(1)_Y$ mixing on the neutral boson mass. The present theorem isolates the strict inequality that follows once $g' > 0$.
proof idea
The tactic proof first unfolds the sibling definitions mW_sq and mZ_sq. It then obtains 0 < v^2 and 0 < gp^2 by the positivity tactic, forms their product, and feeds the positive term into nlinarith to conclude that the difference equals (gp^2 v^2)/4 > 0.
why it matters
The result is packaged inside the ElectroweakMassBridgeCert record (the single downstream user), which assembles all gauge-mass facts for the Standard Model embedding. It supplies the mass-ordering step that complements the RS-specific Weinberg-angle prediction sin^2 theta_W = (3 - phi)/6 proved in the companion ElectroweakMasses module. The remaining open task is numerical calibration of g and g' from the phi-ladder, kept separate from this unconditional bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.