sc_product
plain-language theorem explainer
The RS Weinberg angle satisfies sin²θ_W cos²θ_W = (8−φ)/36 exactly. Anyone assembling the electroweak zero-parameter scorecard or the tree-level VEV relation cites this identity. The proof is a one-line wrapper of the algebraic product lemma already proved in VEVConsistency.
Claim. With the RS Weinberg angle $\sin^2\theta_W = (3-\varphi)/6$ and $\cos^2\theta_W = 1 - \sin^2\theta_W$, one has $\sin^2\theta_W \cdot \cos^2\theta_W = (8-\varphi)/36$.
background
The electroweak zero-parameter scorecard contrasts SM's four free inputs (g, g', v, λ) with RS, where all four are forced: α from the T5/T6/T7 chain, sin²θ_W from gauge-embedding geometry, m_Z from the φ-ladder, and v from the tree-level relation involving the product sin²θ_W cos²θ_W.
RS fixes $\sin^2\theta_W^{\mathrm{RS}} = (3-\varphi)/6$ and $\cos^2\theta_W^{\mathrm{RS}} = 1 - \sin^2\theta_W^{\mathrm{RS}}$. The golden ratio obeys $\varphi^2 = \varphi + 1$. The upstream lemma sin2_cos2_product already records the elementary expansion $(3-\varphi)/6 \cdot (3+\varphi)/6 = (9-\varphi^2)/36 = (8-\varphi)/36$.
proof idea
One-line term proof: apply the upstream theorem sin2_cos2_product from VEVConsistency, which unfolds the two angle definitions and uses φ² = φ + 1 to reduce the product to (8−φ)/36.
why it matters
This identity is one of the four certified fields of ElectroweakZeroParamScoreCardCert. The parent theorem electroweakZeroParamScoreCardCert_holds packages it with the SM/RS parameter counts and the α band to assert that RS contributes zero free electroweak parameters. It is the algebraic link between the geometric sin²θ_W = (3−φ)/6 and the tree-level VEV formula v² = m_Z² sin²θ_W cos²θ_W α⁻¹/π listed in the module doc. Landmark contact: φ from T6; the angle itself is the gauge-embedding input of the scorecard, not a free fit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.