wz_masses_positive
plain-language theorem explainer
The theorem asserts strict positivity of the W and Z boson masses in the Recognition Science electroweak sector. Gauge-boson spectrum calculations and vacuum-expectation-value derivations cite it to guarantee physical scales. The proof is a short term-mode extraction that rewrites the absolute-value bounds from w_mass_near_80 and z_mass_near_91 into lower bounds via linear arithmetic.
Claim. $0 < m_W$ and $0 < m_Z$, where $m_W = 80.3692$ GeV and $m_Z$ is the corresponding Z-boson mass in GeV.
background
In the ElectroweakBosons module the W and Z masses are fixed numerical constants derived from the RS phi-ladder placement of the Higgs vacuum expectation value. The upstream theorems w_mass_near_80 and z_mass_near_91 supply the concrete bounds |m_W - 80| < 1 and |m_Z - 91| < 1. These rest on the anchor definitions W and Z that map charge sectors to integer defect counts, together with the CirclePhaseLift.and lemma that controls angular Lipschitz constants on the phase circle.
proof idea
One-line wrapper that imports the two approximate-mass theorems, rewrites their absolute-value statements with abs_lt, splits the conjunction, and finishes both goals by linarith on the left-hand sides of the resulting inequalities.
why it matters
Positivity is required by the downstream theorem vev_not_equal_higgs_mass to separate the electroweak scale from the Higgs mass and to keep the vacuum expectation value strictly positive. It closes the electroweak sector of the T5-T8 forcing chain by ensuring the gauge-boson rung on the phi-ladder lies above zero, consistent with the J-cost minimum that sets the observed 80-91 GeV window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.