sin2_lt
plain-language theorem explainer
The RS Weinberg angle satisfies sin²θ_W < 0.231, with sin²θ_W = (3−φ)/6. Anyone checking the W-boson absolute mass scorecard cites this upper half of the sin² band. The proof unfolds the closed form, inserts a strict lower bound φ > 1.614 from √5, and finishes by linear arithmetic.
Claim. With the Recognition Science Weinberg angle $\sin^2\theta_W^{\mathrm{RS}} = (3-\varphi)/6$, one has $\sin^2\theta_W^{\mathrm{RS}} < 0.231$.
background
This module builds a first-principles W-boson mass scorecard: every input is forced by the RS chain, with zero fitted parameters. The chain is $m_Z$ on the phi-ladder (rung 51), the geometric Weinberg angle $\sin^2\theta_W = (3-\varphi)/6$, and $m_W = m_Z\sqrt{1-\sin^2\theta_W}$.
The golden ratio $\varphi$ is the self-similar fixed point forced at T6. The electroweak mass module defines $\sin^2\theta_W^{\mathrm{RS}} := (3-\varphi)/6$ as the gauge-embedding value of the mixing angle. Sibling bounds place $\cos^2\theta_W$ in $(0.769,0.771)$ and prove $m_W/m_Z = \cos\theta_W$ at tree level.
The present inequality is the upper edge of the $\sin^2$ band used by the scorecard certificate.
proof idea
Unfold $\sin^2\theta_W^{\mathrm{RS}}$ to $(3-\varphi)/6$. Establish the strict lower bound $\varphi > 1.614$ by comparing $\sqrt{5}$ against $2.228$: rewrite $2.228$ as $\sqrt{2.228^2}$ (nonnegativity), apply monotonicity of square root, then rearrange the definition $\varphi = (1+\sqrt{5})/2$ by linarith. A second linarith converts $\varphi > 1.614$ into $(3-\varphi)/6 < 0.231$. No external lemmas beyond the definition of $\varphi$ and basic real arithmetic.
why it matters
Feeds directly into wBosonAbsoluteScoreCardCert_holds, which packages the closed-form $\cos^2$, the $\cos^2$ and $\sin^2$ bands, the $m_W/m_Z = \cos\theta_W$ identity, and the zero-free-parameter claim. Together with the matching lower bound, this pins $\sin^2\theta_W^{\mathrm{RS}}$ inside a narrow interval around the geometric value $(3-\varphi)/6$.
In the broader framework the angle is not fitted: it is fixed by gauge-embedding geometry once $\varphi$ is forced (T6). The scorecard then predicts a tree-level $m_W$ band near $79.92,\mathrm{GeV}$; the residual versus PDG is attributed to radiative running of $\alpha$, not to free parameters. This lemma is the upper half of that numerical control.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.