cos2_lt
plain-language theorem explainer
The RS Weinberg cosine-squared is strictly below 0.771. Anyone building the absolute W-mass scorecard cites this as the upper half of the cos²θ_W band. The proof rewrites to the closed form (3+φ)/6 and finishes by linear arithmetic from the elementary bound φ < 1.62.
Claim. The Recognition Science value of $\cos^2\theta_W$ obeys $\cos^2\theta_W < 0.771$. Equivalently, with the closed form $\cos^2\theta_W=(3+\varphi)/6$ and the golden-ratio fixed point $\varphi$, one has $(3+\varphi)/6 < 0.771$.
background
The W-boson absolute mass scorecard derives $m_W$ from first principles with zero fitted parameters. The chain is: $m_Z$ from the phi-ladder (electroweak rung 51), the RS Weinberg angle $\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}$.
Here $\cos^2\theta_W$ is defined as $1-\sin^2\theta_W$. The sibling closed-form theorem rewrites that definition to $(3+\varphi)/6$. The constant $\varphi$ is the self-similar fixed point forced at T6; the upstream bound $\varphi<1.62$ follows from $\sqrt{5}<2.24$.
The module targets a tree-level band $m_W\in(79921,79922)$ MeV, with the residual to PDG attributed to radiative corrections rather than free parameters.
proof idea
One short tactic proof. Rewrite the RS cosine-squared via the closed-form identity $\cos^2\theta_W=(3+\varphi)/6$. Bring in the constant lemma $\varphi<1.62$. Linear arithmetic then closes $(3+\varphi)/6<4.62/6=0.77<0.771$.
why it matters
Supplies the upper edge of the cos² band inside the scorecard certificate, which packages the closed form, both cos² and sin² bands, the identity $m_W/m_Z=\cos\theta_W$, and the zero-free-parameter claim. Together with the matching lower bound it pins $\cos^2\theta_W\in(0.769,0.771)$, the geometric input to the absolute tree-level $m_W$ prediction. Downstream of T6 (φ forced) and the electroweak ladder; the residual versus PDG is left to alpha running, not adjustable constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.