cos2_theta_W_rs_eq
plain-language theorem explainer
The equality establishes that the RS-predicted value of cos²θ_W equals (3 + φ)/6. Researchers deriving W boson masses from the Z boson rung in the electroweak sector would cite this identity when applying the gauge relation m_W = m_Z cos θ_W. The proof is a one-line wrapper that unfolds the cosine and sine definitions then normalizes via ring.
Claim. $cos^2 θ_W = (3 + φ)/6$, where φ denotes the golden ratio and the left-hand side is defined as 1 minus the RS prediction sin²θ_W = (3 − φ)/6.
background
The ElectroweakMasses module differentiates boson masses on the phi-ladder: the Z boson sits at rung 1 with m_Z = 2 × φ^51 / 10^6 MeV, while the W boson follows from the Weinberg angle via m_W = m_Z cos θ_W. The module doc states that sin²θ_W = (3 − φ)/6 supplies the zero-parameter RS prediction. cos2_theta_W_rs is defined as 1 − sin2_theta_W_rs and sin2_theta_W_rs as (3 − Constants.phi)/6. The upstream Constants structure from LawOfExistence bundles the CPM constants including phi.
proof idea
This is a one-line wrapper proof. It unfolds the definitions of cos2_theta_W_rs and sin2_theta_W_rs, then applies the ring tactic to obtain the algebraic identity.
why it matters
The equality supplies the algebraic closure required for the W boson mass formula inside the ElectroweakMasses module. It supports the zero-parameter derivation of m_W from m_Z using the RS Weinberg angle and sits within the phi-ladder mass formula and the eight-tick octave structure. No downstream theorems currently reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.