sin2_W_pos
plain-language theorem explainer
The RS-derived weak mixing angle squared is strictly positive. Gauge-hierarchy and electroweak scorecard proofs cite this to keep sin²θ_W inside (0,1). The argument unfolds the closed form (3−φ)/6 and applies a decimal upper bound φ < 1.6180340 so the numerator is positive while the denominator is the constant 6.
Claim. With $\varphi$ the golden ratio and $\sin^2\theta_W^{\mathrm{RS}}=(3-\varphi)/6$, one has $0<\sin^2\theta_W^{\mathrm{RS}}$.
background
In the gauge-coupling hierarchy scorecard the three Standard Model couplings are fixed by the Recognition Science forcing chain with no free parameters. Electromagnetic strength sits in the narrow band $\alpha^{-1}_{\mathrm{EM}}\in(137.030,137.039)$; the weak sector is tied to it by the closed form $\sin^2\theta_W=(3-\varphi)/6$; the strong coupling is $\alpha_s=\varphi^{-3}/\pi$, and the three inverse couplings sum to $12\pi$.
Here $\varphi$ is the golden ratio forced as the self-similar fixed point (T6). The local definition is simply $\sin^2\theta_W^{\mathrm{RS}}:=(3-\varphi)/6$. Positivity of this quantity is the elementary arithmetic claim that the numerator $3-\varphi$ is positive, which follows once $\varphi$ is known to lie below 2 (in fact well below 1.62).
Upstream decimal bounds supply $\varphi<1.6180340$ by comparing $\sqrt{5}$ against a tight rational square.
proof idea
Unfold the definition to $(3-\varphi)/6$. Apply the positivity-of-quotient lemma: it suffices that the numerator and the denominator are both positive. The denominator is the literal constant 6, discharged by norm_num. For the numerator, import the W8/PhiBounds theorem $\varphi<1.6180340$ and finish with a one-line linear arithmetic comparison against 3.
why it matters
The parent certificate gaugeCouplingHierarchyScoreCardCert_holds packages five elementary facts about the RS gauge hierarchy; this positivity lemma is the field sin2_positive of that structure. Together with the companion bound $\sin^2\theta_W<1$ it pins the weak mixing angle inside the open unit interval, which is required before one can compare electromagnetic and weak couplings or assert the zero-free-parameter claim of the scorecard.
In the broader framework the formula $\sin^2\theta_W=(3-\varphi)/6$ is the bridge between the electromagnetic $\alpha$-band and the weak sector, sitting downstream of T5–T6 (J-uniqueness and $\varphi$ forced). The module records Lean status 0 sorry / 0 axiom, so this lemma is part of the closed arithmetic spine rather than scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.