mW_over_mZ_eq_cos_thetaW
plain-language theorem explainer
The theorem proves that the ratio of W-boson to Z-boson masses equals the square root of the standard-model cosine-squared Weinberg angle, for positive gauge coupling g, non-negative g-prime, and positive electroweak scale v. Electroweak physicists would cite this result when connecting recognition-derived scales to tree-level SM mass relations. The proof unfolds the squared-mass definitions, establishes their positivity, applies the square-root division identity, and reduces to the squared-ratio lemma.
Claim. Let $g, g', v$ be real numbers with $g > 0$, $g' ≥ 0$, $v > 0$. Then $m_W(g,v)/m_Z(g,g',v) = √(cos² θ_W^SM(g,g')), where the masses are defined by $m_W² = g² v²/4$ and $m_Z² = (g² + g'²) v²/4$, and cos² θ_W^SM denotes the standard-model expression $g²/(g² + g'²)$.
background
This module formalizes the tree-level electroweak gauge-boson masses from the recognition substrate scale v together with arbitrary positive gauge couplings g and g'. The defining relations are m_W² = g² v² / 4 and m_Z² = (g² + g'²) v² / 4, which immediately imply the ratio m_W / m_Z = g / √(g² + g'²) and the Weinberg angle definitions sin² θ_W = g'² / (g² + g'²). The present theorem supplies the mass-form version of the ratio identity under the stated positivity hypotheses.
proof idea
The tactic proof first unfolds the definitions of mW and mZ. It then establishes strict positivity of mW_sq g v and mZ_sq g gp v via positivity and linarith tactics on the squared terms. Non-negativity follows immediately. The ratio of square roots is rewritten using Real.sqrt_div, after which congruence reduces the claim to the squared identity mW_over_mZ_sq_eq_cos_sq g gp v hg hv.
why it matters
This declaration completes the gauge-mass bridge in the ElectroweakMassBridge module, providing the unconditional theorem that m_W / m_Z equals cos θ_W for any admissible positive couplings. It sits inside the master certificate for W/Z relations and connects the RS substrate v (from HiggsEFTBridge) to standard-model phenomenology. The numerical identification of g and g' with RS predictions remains open, as noted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.