w_mass_near_80
plain-language theorem explainer
The W boson mass derived from the Recognition Science electroweak sector satisfies an absolute deviation of less than 1 GeV from 80. Researchers comparing RS mass predictions to collider measurements near 80.4 GeV would cite this bound during validation of the weak sector. The proof reduces the statement to the explicit mass definition by simplification and confirms the numerical inequality by direct evaluation.
Claim. $|m_W - 80| < 1$, where $m_W$ denotes the W boson mass in GeV obtained from the vacuum expectation value placed on the phi-ladder after electroweak symmetry breaking.
background
The module derives W and Z boson masses from the Higgs mechanism interpreted in Recognition Science, with electroweak symmetry breaking corresponding to a J-cost minimum. The weak mixing angle arises from the geometric embedding of the gauge groups, producing the relation $m_Z = m_W / cos θ_W$. The vacuum expectation value occupies a definite rung on the phi-ladder, fixing the electroweak scale near 246 GeV and generating the listed predictions $m_W ≈ 80.38$ GeV, $m_Z ≈ 91.19$ GeV, and $sin²θ_W ≈ 0.231$ (module documentation). Upstream anchor maps assign integer charges to lepton and quark sectors that enter the mass construction.
proof idea
The proof is a one-line wrapper that applies simplification to unfold the definition of the W boson mass in GeV units and then invokes numerical normalization to verify the absolute difference from 80 is strictly less than 1.
why it matters
This numerical verification anchors the W mass prediction and is invoked directly by the downstream theorem establishing strict positivity of both W and Z masses. It supplies the concrete check required by the module's derivation steps labeled P-015, P-016, and C-004. The result is consistent with the phi-ladder mass formula and the eight-tick octave that sets the electroweak scale in the broader Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.