cos_theta_W
plain-language theorem explainer
Cosine of the Weinberg angle follows from the supplied sin²θW via the trigonometric identity in the electroweak sector. Researchers verifying W/Z mass ratios in Recognition Science cite it when checking the predicted ratio against the experimental 0.881 value. The definition is a direct algebraic expression that applies the square root to one minus the fixed sin²θW input.
Claim. $cos θ_W = √(1 - sin²θ_W)$ where sin²θ_W is the on-shell weak mixing parameter fixed at 0.23122.
background
The module derives electroweak boson masses from the RS mechanism in which the Higgs VEV breaks SU(2)_L × U(1)_Y to U(1)_EM, with the weak mixing angle emerging from the gauge embedding. The J-cost minimum sets the symmetry-breaking scale and places the VEV near 246 GeV on the phi-ladder. Upstream sin²θ_W is supplied numerically as 0.23122 in the same module and equivalently as (3 - phi)/6 in BosonVerification.
proof idea
One-line definition that applies the square root to one minus the sibling sin2_theta_W value.
why it matters
This supplies the cosine factor required by the mass relation in predicted_z_from_w and by the verification theorem wz_ratio_equals_cos_theta, which shows the numerical W/Z ratio lies within 0.005 of cos θ_W. It supports the module predictions m_W ≈ 80.38 GeV, m_Z ≈ 91.19 GeV and the phi-ladder placement of the electroweak scale, closing the loop from the gauge structure to the observed boson masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.