wz_ratio_bounds
plain-language theorem explainer
Physicists modeling electroweak masses in Recognition Science cite this result to place the squared W/Z mass ratio strictly between 0.7696 and 0.7698. The interval follows from the Weinberg angle expressed as (3 + phi)/6. The proof is a one-line wrapper that rewrites the ratio to cos squared theta W and invokes the pre-established bounds on that quantity.
Claim. $0.7696 < (3 + phi)/6 < 0.7698$, where the middle term equals cos² theta_W and phi is the golden ratio.
background
In the BosonVerification module the electroweak sector fixes B_pow = 1 and r0 = 55, so boson masses sit on the phi-ladder via m(EW, r) = 2 * phi^{50+r} / 10^6 MeV. The Weinberg angle is introduced as sin² theta_W = (3 - phi)/6, which immediately yields cos² theta_W = (3 + phi)/6. wz_mass_ratio_sq is the definition (3 + Constants.phi)/6. The sibling theorem wz_ratio_eq_cos2 states that this quantity equals cos2_theta_W. The upstream result cos2_theta_W_bounds supplies the numerical interval (0.7696, 0.7698) for cos2_theta_W by unfolding the definition and applying linear arithmetic to the bounds on sin2_theta_W.
proof idea
The proof is a one-line wrapper. It rewrites the target using wz_ratio_eq_cos2 to replace wz_mass_ratio_sq by cos2_theta_W, then applies cos2_theta_W_bounds directly.
why it matters
The declaration closes a verification step inside the electroweak sector of the Recognition framework. It confirms that the phi-derived Weinberg angle produces a mass ratio consistent with the boson rung assignments on the ladder. The module treats experimental PDG values as imported constants rather than derived quantities, so the bound functions as a consistency check rather than a derivation from the T0-T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.