m_Z_exp
plain-language theorem explainer
The experimental Z boson mass is fixed at 91187.6 MeV to serve as the benchmark for RS electroweak predictions. Researchers comparing the rung-1 mass formula against PDG data cite this constant when checking relative error bounds. It enters as a direct numerical assignment with no computation or lemmas.
Claim. The experimental Z boson mass is defined by the constant equation $m_{Z,exp} = 91187.6$ (in MeV).
background
The Electroweak Boson Mass Predictions module places the Z boson at rung 1, yielding the RS formula $m_Z = 2 × φ^{51} / 10^6$ MeV, while the W boson follows from the Weinberg angle via $m_W = m_Z × cos(θ_W)$ with the zero-parameter prediction $sin²θ_W = (3 − φ)/6$. This definition supplies the measured anchor used for numerical verification. The upstream sibling definition in BosonVerification rounds the same quantity to 91188.
proof idea
This is a one-line definition that directly assigns the real number 91187.6 to the identifier. No lemmas are invoked and no tactics are executed.
why it matters
The constant anchors the z_relative_error theorem, which certifies that the predicted z_pred satisfies |z_pred − m_Z_exp| / m_Z_exp < 0.0013, and it populates the z_error field inside the EWCert structure. It thereby closes the loop between the rung-1 assignment and experiment, supporting the framework claim of parameter-free electroweak masses and enabling the wz_ratio_exp_comparison that checks consistency with the cosine relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.