cos_theta_W_rs
plain-language theorem explainer
The definition supplies the Recognition Science prediction for the cosine of the Weinberg angle by extracting the positive square root of the companion cosine-squared term. Electroweak mass calculations and verification certificates cite it to enforce the W/Z ratio. It is realized as a direct square-root extraction from the upstream cos2 definition.
Claim. $cos θ_W^{RS} := √(1 - sin²θ_W^{RS})$ where sin²θ_W^{RS} follows the RS formula (3 - φ)/6.
background
The ElectroweakMasses module predicts boson masses from the phi-ladder with the Z boson fixed at rung 1, giving m_Z = 2 φ^51 / 10^6 MeV. The W mass follows the gauge relation m_W = m_Z cos θ_W with the zero-parameter RS prediction sin²θ_W = (3 - φ)/6. The upstream definition sets cos2_theta_W_rs to 1 minus the sine-squared term.
proof idea
One-line definition that applies the real square root to the value of cos2_theta_W_rs.
why it matters
It supplies the cosine factor required by the W boson prediction w_pred and appears in the EWCert structure to enforce the wz_is_cos field. The downstream theorem wz_ratio_eq_cos proves the predicted W/Z ratio equals this cosine by direct unfolding. This completes the electroweak differentiation in the Recognition Science framework, fixing the Weinberg angle via φ without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.