sin_sq_thetaW_SM
plain-language theorem explainer
The definition supplies the Standard Model expression for sin²θ_W directly from the gauge couplings g and g'. Electroweak model builders cite this when relating the W and Z boson masses through the Weinberg angle. It is introduced as a simple algebraic abbreviation without further derivation.
Claim. $sin^2 θ_W = g'^2 / (g^2 + g'^2)$ for real gauge couplings $g, g'$.
background
The Electroweak Mass Bridge module derives the Standard Model gauge-boson mass relations from the recognition-substrate scale v together with generic positive gauge couplings g and g'. The relations are m_W² = g² v² / 4, m_Z² = (g² + g'²) v² / 4, m_W / m_Z = cos θ_W = g / √(g² + g'²), and sin² θ_W = g'² / (g² + g'²). These are the SM tree-level gauge-mass relations, conditional on the same v from the RS substrate and any positive g, g'.
proof idea
This declaration is a direct definition that encodes the Standard Model formula for the square of the sine of the Weinberg angle in terms of the gauge couplings.
why it matters
This definition anchors the electroweak mass relations by providing the gauge-coupling expression for sin²θ_W. It is used by the theorem establishing cos²θ_W + sin²θ_W = 1 for nontrivial gauge couplings and by the master certificate ElectroweakMassBridgeCert that collects all W/Z mass relations. The module distinguishes this unconditional gauge relation from the separate open problem of deriving g and g' numerically from the φ-ladder substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.