z_relative_error
The Recognition Science Z-boson mass prediction deviates from the experimental value by less than 0.13 percent. Particle physicists comparing the phi-ladder mass formula to PDG data would cite this bound when verifying electroweak predictions. The short tactic proof obtains the narrow interval for z_pred from z_mass_bounds, records that m_Z_exp is positive, rewrites the relative-error inequality, and closes with nlinarith.
claimLet $z_{pred}$ be the Recognition Science prediction for the Z-boson mass and $m_{Z,exp}$ the experimental value 91187.6 MeV. Then $|z_{pred}-m_{Z,exp}|/m_{Z,exp}<0.0013$.
background
In the ElectroweakMasses module the Z boson occupies rung 1 of the phi-ladder, giving the explicit mass formula $m_Z=2φ^{51}/10^6$ MeV. The upstream theorem z_mass_bounds supplies the tight interval (91075.09,91075.10) MeV for this prediction. The experimental anchor m_Z_exp is defined as 91187.6 MeV, and the present result quantifies the relative discrepancy between them.
proof idea
The proof first obtains the interval bounds on z_pred from z_mass_bounds. It records that m_Z_exp is positive by unfolding its definition and applying norm_num. The target inequality is rewritten via div_lt_iff₀ and abs_lt, after which nlinarith closes both sides of the estimate using the supplied interval.
why it matters in Recognition Science
This theorem supplies the z_error field of the EWCert record constructed in ew_cert_exists, thereby certifying the entire electroweak mass sector. It closes the verification that the Recognition Science phi-ladder reproduces the Z boson to better than 0.13 percent accuracy, consistent with the zero-parameter Weinberg angle derived from the same framework. The result supports the mass formula yardstick·φ^(rung-8+gap(Z)) in the electroweak sector.
scope and limits
- Does not claim exact numerical equality between prediction and experiment.
- Does not extend the bound to the W or Higgs boson masses.
- Does not incorporate radiative corrections or higher-order effects.
- Does not apply outside the Z boson in the electroweak sector.
Lean usage
have hz_err : |z_pred - m_Z_exp| / m_Z_exp < 0.0013 := z_relative_errorformal statement (Lean)
109theorem z_relative_error :
110 |z_pred - m_Z_exp| / m_Z_exp < 0.0013 := by
proof body
Tactic-mode proof.
111 have hb := z_mass_bounds
112 have hexp_pos : (0 : ℝ) < m_Z_exp := by unfold m_Z_exp; norm_num
113 rw [div_lt_iff₀ hexp_pos, abs_lt]
114 unfold m_Z_exp
115 constructor <;> nlinarith [hb.1, hb.2]
116
117/-! ## W Boson Mass — Z × cos(θ_W)
118
119m_W = m_Z × cos(θ_W) where cos²(θ_W) = (3+φ)/6 -/
120