cos_sq_plus_sin_sq_thetaW
plain-language theorem explainer
The identity cos² θ_W + sin² θ_W = 1 holds for the Weinberg angle defined from positive real gauge couplings g and g' via the standard expressions cos² θ_W = g²/(g² + g'²) and sin² θ_W = g'²/(g² + g'²). Electroweak model builders cite this when confirming tree-level consistency of the W and Z mass relations. The proof unfolds the two rational definitions, checks that the common denominator is positive and nonzero, then applies field simplification to reduce the sum directly to 1.
Claim. For real numbers $g, g'$ with $g > 0$, define $c = g^2 / (g^2 + {g'}^2)$ and $s = {g'}^2 / (g^2 + {g'}^2)$. Then $c + s = 1$.
background
The Electroweak Mass Bridge module derives the 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, m_Z² = (g² + g'²) v² / 4, the ratio m_W / m_Z = g / √(g² + g'²), and the Weinberg-angle definitions cos² θ_W = g² / (g² + g'²), sin² θ_W = g'² / (g² + g'²). These relations are conditional on the same v supplied by HiggsEFTBridge and on g, g' > 0; numerical values for the couplings remain an empirical input separate from the substrate calibration. The sibling definitions cos_sq_thetaW_SM and sin_sq_thetaW_SM supply exactly these rational expressions.
proof idea
The tactic proof first unfolds cos_sq_thetaW_SM and sin_sq_thetaW_SM to expose the explicit fractions. It then obtains 0 < g² by positivity, 0 ≤ g'² by squaring, and 0 < g² + g'² by linarith. The nonzero-denominator fact follows immediately, after which field_simp cancels the common positive denominator and yields 1.
why it matters
This result normalizes the Weinberg-angle definition inside the Electroweak Mass Bridge and is invoked by electroweakMassBridgeCert to certify the full set of gauge-mass relations. It supplies the gauge-relation half of the module's THEOREM status for all positive (g, g', v), remaining valid independently of the companion recognition prediction sin² θ_W = (3 − φ)/6. The numerical calibration of g and g' from the RS substrate is left open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.