m_W
plain-language theorem explainer
The declaration supplies the numerical value of the W boson mass in GeV for Recognition Science calculations of electroweak ratios. Researchers comparing RS phi-ladder predictions to ATLAS and CDF data would cite this constant when anchoring mass hierarchies. The definition is a direct numerical assignment with no computation or lemmas required.
Claim. The W boson mass is fixed at $m_W = 80.377$ GeV as the numerical anchor for the electroweak sector on the phi-ladder.
background
The StandardModel.WZMassRatio module positions W and Z masses within the phi-quantized gauge structure of Recognition Science, where the observed ratio m_W / m_Z approximates cos(theta_W) and emerges from SU(2) x U(1) mixing constrained by the golden ratio. Upstream, the Z definition from Masses.Anchor supplies an integer map Z(sector, Q) that computes anchor relations for leptons and quarks via powers of a scaled charge Q6, while the certified version in AnchorPolicyCertified simply aliases this map to species. The module doc sets the local setting as SM-003, targeting derivation of the W/Z ratio from phi-structure with measured values m_W approx 80.4 GeV and m_Z approx 91.2 GeV.
proof idea
The definition is a direct constant assignment of the measured W boson mass value. No lemmas are applied and no tactics are used beyond the literal real number 80.377.
why it matters
This definition supplies the numerical input for downstream theorems including vev_wz_mass_hierarchy and w_mass_from_z, which relate the VEV to W and Z masses through the phi-ladder, and hierarchy_problem_dissolution, which shows the hierarchy problem dissolves because all scales sit on discrete phi-rungs. It anchors the electroweak parameters in the forcing chain landmarks T5 J-uniqueness and T6 phi fixed point, supporting the paper proposition on electroweak parameters from RS. It touches the open question of whether the exact 80.377 value receives a closed-form phi-ladder expression.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.