mW_over_mZ_sq_eq_cos_sq
plain-language theorem explainer
The theorem establishes that the squared-mass ratio of the W and Z bosons equals cos² θ_W under the Standard-Model definition from the gauge couplings g and g'. Electroweak physicists bridging recognition-scale vacuum expectation values to gauge-boson masses would invoke this identity when assembling the tree-level relations. The proof is a one-line wrapper that rewrites via the prior squared-ratio identity and closes by reflexivity.
Claim. For real numbers $g, g', v$ with $g > 0$ and $v > 0$, the ratio of the squared W-boson mass to the squared Z-boson mass equals $g^2 / (g^2 + g'^2)$, where $m_W^2 = g^2 v^2 / 4$, $m_Z^2 = (g^2 + g'^2) v^2 / 4$, and the right-hand side is the SM definition of $cos^2 θ_W$.
background
In the Electroweak Mass Bridge module the W-boson mass squared is defined by $m_W^2(g, v) = g^2 v^2 / 4$ and the Z-boson mass squared by $m_Z^2(g, g', v) = (g^2 + g'^2) v^2 / 4$, with $v$ the recognition-substrate scale supplied by the Higgs EFT bridge. The cosine squared of the Weinberg angle is defined by $cos^2 θ_W = g^2 / (g^2 + g'^2)$. The upstream theorem mW_over_mZ_sq already shows that the mass-squared ratio equals $g^2 / (g^2 + g'^2)$ for positive $g$ and $v$. The module therefore formalizes the SM tree-level gauge-mass relations conditional on positive gauge couplings and the shared $v$.
proof idea
The proof is a one-line wrapper that applies the theorem mW_over_mZ_sq g gp v hg hv to obtain the ratio equal to $g^2 / (g^2 + gp^2)$, then uses reflexivity to match the definition of cos_sq_thetaW_SM.
why it matters
This result supplies the squared-ratio identity required by the ElectroweakMassBridgeCert certificate and by the follow-on theorem mW_over_mZ_eq_cos_thetaW. It completes the gauge-relation half of the bridge, showing that any positive $(g, g')$ yield the SM tree-level relation $m_W / m_Z = cos θ_W$ once the mass definitions are inserted. The module leaves open the numerical calibration of $g$ and $g'$ from the recognition substrate, tracked separately under OPEN_NORMALIZATION.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.