wz_ratio_eq_cos2
plain-language theorem explainer
The identity equates the squared W/Z mass ratio to cos² of the Weinberg angle, both written as explicit functions of the golden ratio phi. Electroweak mass verifiers cite it to confirm that the phi-ladder rung assignments reproduce the standard mixing relation without extra assumptions. The proof is a one-line algebraic reduction obtained by unfolding the three definitions and invoking ring.
Claim. Let $phi$ denote the golden ratio. With $sin^2 theta_W := (3 - phi)/6$, the squared W/Z mass ratio equals $(3 + phi)/6$ and $cos^2 theta_W := 1 - sin^2 theta_W$. Then $(3 + phi)/6 = 1 - (3 - phi)/6$.
background
In the electroweak sector the module assigns W, Z and Higgs bosons to rungs on the phi-ladder via the formula m(EW, r) = 2 * phi^{50+r} / 10^6 MeV. The Weinberg angle is fixed by the definition sin2_theta_W := (3 - Constants.phi)/6, which yields the relation M_Z = M_W / cos theta_W. The sibling definitions then introduce cos2_theta_W := 1 - sin2_theta_W and wz_mass_ratio_sq := (3 + Constants.phi)/6 as noncomputable reals.
proof idea
The term proof unfolds wz_mass_ratio_sq, cos2_theta_W and sin2_theta_W, then applies the ring tactic to reduce the resulting rational expressions in phi to an identity.
why it matters
The equality is used to build the BosonVerificationCert and to discharge the numerical bounds in wz_ratio_bounds. It supplies the algebraic step that links the phi-derived sin² theta_W to the expected cos² theta_W relation required by electroweak symmetry. Within the Recognition framework the step supports verification that the W and Z bosons sit on consistent rungs of the eight-tick octave ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.