The definition supplies the W to Z boson mass ratio as the quotient of their masses in the reals. Electroweak model builders cite it when matching RS predictions to the observed value near 0.881. It is introduced by a direct division with no further reduction.
claimThe W/Z mass ratio is defined by $m_W / m_Z$, where $m_W$ and $m_Z$ are the masses of the W and Z gauge bosons.
background
In module SM-003 the W/Z mass ratio is extracted from Recognition Science's φ-structure. The bosons carry masses near 80.4 GeV and 91.2 GeV; their ratio equals cos(θ_W) by definition of the Weinberg angle. Upstream, RSNativeUnits.Mass is an alias for the reals, while GaugeBosonMassesFromRS supplies the companion expression 6/(3 + φ) under φ-quantization of the gauge sector.
proof idea
The declaration is a one-line definition that forms the ratio by dividing the W mass by the Z mass.
why it matters in Recognition Science
This definition anchors the electroweak ratio inside the Recognition framework and supplies the input to GaugeBosonMassCert, which records positivity, the inequality greater than one, and the sin²θ_W band (0.228, 0.232). It also populates the WZBosonRatioScoreCard bracket (0.87, 0.89) and the mass hierarchy statements in ThreeGenerations. The construction sits at the T5–T8 segment of the forcing chain, where φ fixes the self-similar scale and D = 3 emerges.
scope and limits
Does not embed experimental error bars or uncertainties.
Does not derive the numerical value from the φ-ladder inside this declaration.
Does not prove any inequality or certification; those reside in separate theorems.
Does not address neutrino or three-generation extensions.
formal statement (Lean)
53noncomputable def massRatio : ℝ := m_W / m_Z
proof body
Definition body.
54 55/-- **THEOREM**: Mass ratio is approximately 0.88. -/
used by (13)
From the project-wide theorem graph. These declarations reference this one in their body.