z_heavier_than_w
plain-language theorem explainer
z_heavier_than_w establishes that the Z boson mass exceeds the W boson mass under the Recognition Science electroweak assignments. Researchers checking gauge-boson hierarchies in the weak sector would cite this inequality to confirm the observed ordering. The proof reduces directly to unfolding the two constant definitions and applying numerical comparison.
Claim. The Z-boson mass in GeV exceeds the W-boson mass: $m_Z > m_W$ where $m_Z = 91.1876$ and $m_W = 80.3692$.
background
The ElectroweakBosons module derives W and Z masses from the Higgs vacuum expectation value and weak mixing angle in the Recognition Science setting. The module states that electroweak symmetry breaking corresponds to a J-cost minimum, producing the mass relation $m_Z = m_W / cos(θ_W)$ together with the numerical predictions $m_W ≈ 80.38$ GeV and $m_Z ≈ 91.19$ GeV. The upstream definitions supply the explicit constants wBosonMass_GeV := 80.3692 and zBosonMass_GeV := 91.1876.
proof idea
The term proof applies simp to unfold the two mass definitions, then invokes norm_num to verify the concrete numerical inequality 91.1876 > 80.3692.
why it matters
The result feeds the downstream theorem wz_masses_not_equal, which records that the W and Z masses are non-degenerate. It supplies a basic consistency check for the electroweak sector derivations, aligning with the RS mass relation and the phi-ladder placement of the VEV. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.