cos2_theta_W_rs
plain-language theorem explainer
The definition supplies the RS value of cos²θ_W as one minus the predicted sin²θ_W. Electroweak mass calculations cite it to obtain m_W from m_Z via the gauge relation. It is realized as a direct subtraction from the companion sine-squared definition.
Claim. $cos^2 θ_W^{RS} := 1 - sin^2 θ_W^{RS}$ where $sin^2 θ_W^{RS} = (3 - φ)/6$.
background
The ElectroweakMasses module places the Z boson at rung 1 on the phi-ladder, so that m_Z equals 2 φ^51 / 10^6 MeV. The Weinberg angle is fixed by the zero-parameter relation sin²θ_W = (3 - φ)/6. The upstream definition sin2_theta_W_rs records this value exactly.
proof idea
One-line definition that subtracts the sine-squared value from unity.
why it matters
This definition completes the gauge relation m_W = m_Z cos θ_W inside the Recognition Science mass ladder. It is invoked by the positivity theorem cos2_theta_positive and by the algebraic identity cos2_theta_W_rs_eq that rewrites the quantity as (3 + φ)/6. The step supports the T7 eight-tick octave and the D = 3 spatial dimensions built into the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.