wz_ratio_lt_one
plain-language theorem explainer
The theorem establishes that the W to Z boson mass ratio is strictly less than one using the numerical values assigned in the electroweak sector. Particle physicists verifying mass hierarchies from the weak mixing angle would cite this result. The proof is a direct term-mode reduction that unfolds the ratio definition and applies numerical normalization to confirm the inequality.
Claim. The ratio of W boson mass to Z boson mass satisfies $m_W / m_Z < 1$, where $m_W = 80.3692$ GeV and $m_Z = 91.1876$ GeV.
background
In the ElectroweakBosons module the W boson mass is defined as the constant 80.3692 GeV and the Z boson mass as 91.1876 GeV. Their ratio is introduced as the quotient of these two constants. The module derives these masses from the Higgs mechanism and weak mixing angle, with the ratio expected to equal cos of the Weinberg angle under the RS gauge embedding.
proof idea
The proof unfolds the definitions of wz_mass_ratio, wBosonMass_GeV and zBosonMass_GeV, then applies norm_num to evaluate the numerical comparison directly.
why it matters
This result confirms the mass hierarchy required by the electroweak predictions in the Recognition Science framework, where the ratio equals cos theta_W and is less than unity. It supports the listed predictions m_W approximately 80.38 GeV and m_Z approximately 91.19 GeV together with the phi-ladder placement of the VEV. No downstream theorems are recorded, yet the inequality anchors the consistency check for the gauge structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.