mW_over_mZ_sq
plain-language theorem explainer
The identity states that the squared W to Z boson mass ratio equals g squared over g squared plus g prime squared for any positive gauge couplings and substrate scale. Electroweak phenomenologists cite it when mapping recognition-derived v to tree-level Standard Model predictions. The proof is a short tactic sequence that unfolds the mass-squared definitions, adds four positivity facts, and finishes with field simplification.
Claim. Let $g, g', v$ be real numbers with $g > 0$ and $v > 0$. Then $m_W^2(g, v) / m_Z^2(g, g', v) = g^2 / (g^2 + {g'}^2)$, where the squared masses are the Standard-Model expressions $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 gauge-boson mass relations from the recognition substrate scale $v$ (imported via HiggsEFTBridge) together with arbitrary positive couplings $g$ and $g'$. The sibling definitions supply $mW_sq g v = g^2 v^2 / 4$ and $mZ_sq g gp v = (g^2 + gp^2) v^2 / 4$, so the ratio identity is immediate once common factors cancel. Upstream results such as SpectralEmergence.of supply the gauge content SU(2) x U(1) while LawOfExistence.Model and PhiForcingDerived.of guarantee the positivity and algebraic closure needed for the field operations.
proof idea
The tactic proof first unfolds mW_sq and mZ_sq. It then introduces four auxiliary facts: positivity of g squared, non-negativity of gp squared, positivity of their sum, and positivity of v squared. Field_simp is applied to the resulting rational expression, which cancels the common v squared over 4 factor and yields the coupling ratio directly.
why it matters
This theorem supplies the algebraic step used by the downstream result mW_over_mZ_sq_eq_cos_sq, which identifies the ratio with cos squared theta_W in the Standard-Model definition. It therefore closes the gauge-mass bridge between the recognition scale v and the observed W and Z masses while remaining agnostic about the numerical values of g and g'. The module doc notes that numerical calibration of those couplings remains an open normalization task separate from this identity. The construction aligns with the forced gauge sector in SpectralEmergence.of and the eight-tick octave structure of the underlying forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.