z_relative_error
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.