sin2_gt
plain-language theorem explainer
The RS Weinberg angle satisfies sin²θ_W = (3-φ)/6 > 0.229. Anyone auditing the tree-level electroweak angle band against PDG would cite this lower bound. The proof unfolds the closed form and finishes by linear arithmetic from the standard upper bound φ < 1.62.
Claim. The Recognition Science Weinberg angle $\sin^2\theta_W=(3-\varphi)/6$ obeys $0.229<\sin^2\theta_W$.
background
This module builds a first-principles W-boson mass scorecard: every input is forced by the RS chain, with zero fitted parameters. The local derivation is $m_Z$ from the phi-ladder (rung 51), $\sin^2\theta_W=(3-\varphi)/6$ from gauge-embedding geometry, and $m_W=m_Z\cos\theta_W=m_Z\sqrt{(3+\varphi)/6}$.
The quantity bounded here is the RS definition $\sin^2\theta_W:=(3-\varphi)/6$. The golden ratio $\varphi$ is the self-similar fixed point of the forcing chain (T6). The only numerical prior needed is the tight upper bound $\varphi<1.62$ (from $\sqrt{5}<2.24$).
proof idea
Unfold the definition to $(3-\varphi)/6$. From the lemma $\varphi<1.62$, obtain the slightly looser comparison $\varphi<1.626$ by linarith, then close $0.229<(3-\varphi)/6$ by another linarith step. No interval arithmetic or external numerics beyond that phi bound.
why it matters
Supplies the lower half of the $\sin^2\theta_W$ band inside wBosonAbsoluteScoreCardCert_holds, which packages the closed-form $\cos^2\theta_W$, the cos and sin bands, the identity $m_W/m_Z=\cos\theta_W$, and the zero-free-parameter claim. Together with the matching upper bound, it pins the tree-level angle that converts the ladder $m_Z$ into the predicted $m_W\in(79921,79922)$ MeV band. The residual versus PDG is attributed to radiative corrections (alpha running), outside this tree-level scorecard.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.