m_Z_exp
plain-language theorem explainer
Experimental Z boson rest mass fixed at 91187.6 MeV (PDG 2024 central value). Mass-comparison and electroweak certificate code cite this constant when measuring relative error of the RS Z prediction. Bare numeric definition; no proof content.
Claim. The PDG 2024 experimental Z boson rest mass is $m_Z^{\mathrm{exp}} = 91187.6\,\mathrm{MeV}$ (equivalently $91.1876\,\mathrm{GeV}$).
background
The MassComparison module is quarantined from the certified RS surface: it imports external PDG numbers and compares them to mass predictions built from the phi-ladder formula
$$m(\mathrm{species}) = \mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}},$$
with coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$ and sector yardsticks from cube geometry.
Sibling constants in the same file pin lepton and light-quark experimental masses the same way. The electroweak layer re-exports this Z value and uses it as the denominator of relative-error bounds. Units are MeV throughout so that GeV-scale bosons and MeV-scale leptons share one real type.
proof idea
Numeric definition only: the real constant is set to 91187.6 by direct assignment. No lemmas, tactics, or algebraic reduction.
why it matters
Feeds the electroweak verification certificate EWCert, which requires both a tight absolute window on the RS Z prediction and a relative error bound
$$|z_{\mathrm{pred}}-m_Z^{\mathrm{exp}}|/m_Z^{\mathrm{exp}}<0.0013.$$
The theorem z_relative_error unfolds this constant and discharges that inequality by interval arithmetic on the predicted mass. Without a single shared experimental anchor, the W/Z ratio check (w_pred/z_pred = cos theta_W_rs) and the 0.13% claim would not be comparable to PDG 2024. The value itself is not derived from the forcing chain (T0–T8) or the Recognition Composition Law; it is the external datum the ladder prediction is scored against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.