cos2_gt
plain-language theorem explainer
The RS Weinberg cosine-squared exceeds 0.769. Anyone citing the W-mass scorecard band or positivity of cos²θ_W needs this lower bound. The proof rewrites to the closed form (3+φ)/6, inserts a decimal lower bound on φ from √5, and finishes by linear arithmetic.
Claim. In RS units, $\cos^2\theta_W^{\mathrm{RS}} > 0.769$. Equivalently, with the closed form $\cos^2\theta_W^{\mathrm{RS}} = (3+\varphi)/6$ and $\varphi > 1.614$, one has $(3+\varphi)/6 > 0.769$.
background
The W boson absolute mass scorecard derives $m_W$ from the RS forcing chain with no 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\cos\theta_W$.
Here $\varphi$ is the golden ratio fixed by T6 as the self-similar fixed point. The RS cosine-squared is defined by $\cos^2\theta_W^{\mathrm{RS}} := 1 - \sin^2\theta_W^{\mathrm{RS}}$. The sibling theorem cos2_theta_W_closed_form rewrites that definition to the explicit rational $(3+\varphi)/6$.
This lower bound is the first half of the certified band $\cos^2\theta_W \in (0.769, 0.771)$ used by the scorecard certificate.
proof idea
Rewrite the goal with the closed-form identity $\cos^2\theta_W^{\mathrm{RS}} = (3+\varphi)/6$. Establish the decimal inequality $\varphi > 1.614$ by unfolding $\varphi = (1+\sqrt{5})/2$, proving $\sqrt{5} > 2.228$ via $\sqrt{,\cdot,}$ monotonicity on the squared bound $2.228^2 < 5$, then applying linarith. A final linarith step lifts $\varphi > 1.614$ to $(3+\varphi)/6 > 0.769$.
why it matters
Feeds directly into cos2_pos (positivity of $\cos^2\theta_W$, required before taking square roots for the W/Z ratio) and into the scorecard certificate wBosonAbsoluteScoreCardCert_holds, where it is half of the cos2_band pair alongside the matching upper bound.
In the module derivation, the tree-level prediction is $m_W = m_Z\sqrt{(3+\varphi)/6}$ with $m_Z$ on the phi-ladder. The decimal band on $\cos^2\theta_W$ is what turns that closed form into a concrete MeV interval (79921, 79922) MeV before radiative corrections. It sits downstream of T6 (φ forced) and the gauge-embedding geometry that fixes $\sin^2\theta_W = (3-\varphi)/6$; no free electroweak fit parameters enter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.