cos_sq_thetaW_SM
plain-language theorem explainer
The definition supplies the Standard Model expression for cos² θ_W in terms of the SU(2) and U(1) gauge couplings g and g'. Researchers bridging recognition-substrate scales to electroweak masses cite it to recover the tree-level W/Z mass ratio from positive gauge couplings. It is introduced as a direct algebraic assignment with no proof obligations.
Claim. $cos^2 θ_W := g^2 / (g^2 + g'^2)$ for gauge couplings $g, g' ∈ ℝ$.
background
This definition sits inside the Electroweak Mass Bridge module, which derives the Standard-Model gauge-boson mass relations from the recognition-substrate scale v together with generic positive gauge couplings g and g'. The module states the tree-level formulas m_W² = g² v² / 4, m_Z² = (g² + g'²) v² / 4, and m_W / m_Z = cos θ_W = g / √(g² + g'²). The electroweak scale v is supplied by the companion HiggsEFTBridge module; positivity of g and g' is an external hypothesis drawn from upstream structures such as LawOfExistence.Model.
proof idea
The declaration is a direct definition that assigns the Standard-Model formula for cos² θ_W without invoking lemmas or tactics.
why it matters
This definition underpins the master certificate ElectroweakMassBridgeCert and the identities mW_over_mZ_eq_cos_thetaW together with mW_over_mZ_sq_eq_cos_sq. It supplies the gauge-relation step that lets any definition of θ_W serve as input while keeping the mass relations unconditional on positive (g, g', v). The open question it touches is numerical calibration of g and g' from the RS substrate, tracked under OPEN_NORMALIZATION.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.