sc_positive
plain-language theorem explainer
The RS Weinberg-angle factors satisfy sin²θ_W · cos²θ_W > 0. Anyone citing the electroweak zero-parameter scorecard needs this positivity to keep the tree-level VEV relation and the scorecard certificate well-defined. The proof is a one-line linear-arithmetic reduction from the stricter lower bound product > 0.176.
Claim. With the RS Weinberg angle $\sin^2\theta_W^{\mathrm{RS}} = (3-\varphi)/6$ and $\cos^2\theta_W^{\mathrm{RS}} = 1 - \sin^2\theta_W^{\mathrm{RS}}$, the product satisfies $0 < \sin^2\theta_W^{\mathrm{RS}}\,\cos^2\theta_W^{\mathrm{RS}}$.
background
The electroweak zero-parameter scorecard contrasts the Standard Model's four free EW inputs $(g,g',v,\lambda)$ with the RS claim that all four are forced. In RS, $\sin^2\theta_W$ is fixed by gauge-embedding geometry as $(3-\varphi)/6$, and $\cos^2\theta_W$ is the complementary factor $1-\sin^2\theta_W$. The tree-level relation $v^2 = m_Z^2\sin^2\theta_W\cos^2\theta_W,\alpha^{-1}/\pi$ then needs that product to be strictly positive so the vacuum expectation value stays in the physical regime.
Upstream, sin2_cos2_gt already proves the sharper numerical bound $\sin^2\theta_W^{\mathrm{RS}}\cdot\cos^2\theta_W^{\mathrm{RS}} > 0.176$, obtained by rewriting the product as $(8-\varphi)/36$ and using $\varphi < 1.62$. Positivity is the coarser consequence needed by the scorecard certificate.
proof idea
One-line term/tactic proof: apply linarith to the upstream inequality sin2_cos2_gt, which states that the same product is strictly larger than $0.176$. Anything above a positive constant is positive, so $0 < \sin^2\theta_W^{\mathrm{RS}}\cdot\cos^2\theta_W^{\mathrm{RS}}$ follows immediately.
why it matters
Feeds the scorecard certificate electroweakZeroParamScoreCardCert_holds, which packages SM-vs-RS parameter counts, the $\alpha$ band, and the sin/cos product identity into a single nonempty certificate of the zero-parameter claim. Module framing: RS derives $\alpha^{-1}$ from the T5/T6/T7 forcing chain, $\sin^2\theta_W$ from geometry, $m_Z$ from the $\varphi$-ladder, and $v$ from the tree-level relation, counting zero free EW parameters against the SM's four. This positivity lemma is the minimal arithmetic guard that the geometric angle factors do not collapse the VEV formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.