wz_mass_ratio_sq
plain-language theorem explainer
Recognition Science sets the squared W to Z boson mass ratio equal to (3 + φ)/6. Researchers verifying electroweak predictions against the Weinberg angle in the phi-ladder framework cite this definition. It is introduced as a direct noncomputable assignment from the phi field in the Constants bundle.
Claim. $ (m_W / m_Z)^2 = (3 + φ)/6 $
background
In the electroweak sector, boson masses occupy rungs on the phi-ladder with B_pow = 1 and r0 = 55. The Weinberg angle satisfies sin²θ_W = (3 − φ)/6, which yields the mass ratio via M_Z = M_W / cos θ_W. The upstream Constants structure from LawOfExistence bundles φ together with parameters such as Knet for use across the framework.
proof idea
This is a direct definition that evaluates to (3 + Constants.phi) / 6 using the phi field from the imported Constants structure. No lemmas or tactics are applied beyond arithmetic evaluation of the expression.
why it matters
The definition supplies the phi-derived value for the W/Z mass ratio squared that is asserted equal to cos²θ_W inside the BosonVerificationCert structure. It implements the electroweak mass formula m(EW, r) = 2 × φ^{50+r} / 10^6 MeV and connects to the phi self-similar fixed point in the T5–T8 forcing chain. The result enables the subsequent bounds theorem wz_ratio_bounds without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.