massRatio
plain-language theorem explainer
The RS expression for the Z to W boson mass ratio is supplied as six divided by three plus phi. Gauge boson mass analyses in the Standard Model cite it when verifying the predicted ratio near 1.13 against data. The assignment is a direct noncomputable definition with no reduction steps.
Claim. The Z-boson to W-boson mass ratio satisfies $m_Z / m_W = 6 / (3 + phi)$, where $phi$ is the golden ratio satisfying $phi^2 = phi + 1$.
background
The Gauge Boson Masses from RS module supplies RS-native expressions for Standard Model parameters, with the module doc stating the ratio equals 6/(3+φ) and sin²θ_W equals (3-φ)/6. Phi denotes the golden ratio, the self-similar fixed point forced as T6 in the UnifiedForcingChain. Upstream, ThreeGenerations defines its massRatio as phi for generational hierarchies scaling as phi, while WZMassRatio defines its massRatio as the experimental m_W/m_Z.
proof idea
The declaration is a one-line definition that directly assigns the constant 6/(3 + phi). No lemmas or tactics are applied.
why it matters
GaugeBosonMassCert depends on this definition to certify the ratio is positive, exceeds one, and lies with sin²θ_W in the band (0.228, 0.232). It also supports WZBosonRatioScoreCard for bracketing the ratio between 0.87 and 0.89. This realizes the phi-ladder prediction for gauge boson masses, linking to T7 eight-tick octave and D=3. No open questions are flagged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.