wz_masses_not_equal
plain-language theorem explainer
Recognition Science assigns distinct masses to the W and Z bosons as part of its electroweak derivation from the Higgs vacuum expectation value. Modelers of symmetry breaking and the weak mixing angle would cite the result to confirm consistency with the observed spectrum. The proof is a one-line term application of the strict inequality between the two pre-defined masses.
Claim. The W boson mass differs from the Z boson mass: $m_W = 80.3692$ GeV and $m_Z = 91.1876$ GeV satisfy $m_W < m_Z$.
background
The module derives electroweak boson masses from the Higgs mechanism after SU(2)_L × U(1)_Y breaking to U(1)_EM, with the vacuum expectation value placed on the phi-ladder. The W and Z masses are fixed by definitions at 80.3692 GeV and 91.1876 GeV respectively, obeying the relation $m_Z = m_W / cos θ_W$ with sin²θ_W ≈ 0.231. This non-degeneracy is required by the gauge embedding and corresponds to the J-cost minimum in the Recognition Science framework.
proof idea
The proof is a one-line term wrapper. It applies the lemma that the Z boson mass exceeds the W boson mass and invokes the not-equal-from-less-than rule on the two real numbers.
why it matters
The result locks in non-degeneracy for the electroweak sector, aligning with the T5 J-uniqueness, T6 phi fixed point, and T8 three-dimensional forcing chain. It underpins the numerical predictions m_W ≈ 80.38 GeV, m_Z ≈ 91.19 GeV and the mass ratio cos θ_W listed in the module documentation for propositions P-015 and P-016. No downstream theorems are recorded in the dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.