z_w_ratio_approx
plain-language theorem explainer
The theorem verifies that the Z to W boson mass ratio lies within 0.01 of 1.135, reproducing the experimental value 91.1876/80.3692 to high accuracy. Electroweak model builders in Recognition Science cite it to confirm the gauge-derived mass relation after symmetry breaking. The proof reduces the claim to direct numerical evaluation of the pre-defined masses via unfolding and normalization.
Claim. $|m_Z / m_W - 1.135| < 0.01$, where $m_Z = 91.1876$ GeV and $m_W = 80.3692$ GeV are the Z and W boson masses.
background
The module derives W and Z masses from the Higgs mechanism in Recognition Science, where electroweak symmetry breaking corresponds to a J-cost minimum and the vacuum expectation value sits at a specific rung on the phi-ladder. The mass relation follows from the gauge embedding: $m_Z = m_W / cos θ_W$, with the ratio testing consistency of the weak mixing angle. Upstream, the scale definition supplies the phi-power placement used for the electroweak VEV, while the individual mass constants fix the numerical targets.
proof idea
One-line wrapper that applies simp to unfold z_w_ratio, zBosonMass_GeV and wBosonMass_GeV, then norm_num to discharge the concrete inequality 91.1876/80.3692 ≈ 1.1346 with error 0.0004.
why it matters
It anchors the electroweak predictions (m_W ≈ 80.38 GeV, m_Z ≈ 91.19 GeV, ratio ≈ 1.135) inside the RS mechanism of symmetry breaking and phi-ladder placement. The result supports the gauge-structure origin of the mass relation without invoking the full forcing chain T0-T8 or RCL directly. No downstream theorems are listed, leaving open whether the numerical match will be upgraded to an exact phi-derived expression.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.