m_Z_exp
plain-language theorem explainer
The m_Z_exp definition supplies the rounded experimental Z boson mass of 91188 MeV as a constant for ratio and error checks in electroweak verification. Researchers comparing Recognition Science phi-ladder predictions against PDG data cite this value directly. It is introduced as a bare constant definition with no lemmas or computation steps.
Claim. Define the experimental Z boson mass by the constant assignment $m_Z^exp := 91188$ (in MeV).
background
The module imports experimental boson masses as quarantined constants separate from Recognition Science derivations. The electroweak formula is $m(EW,r) = 2 φ^{50+r}/10^6$ MeV with rung integers for W, Z and Higgs; the Weinberg angle satisfies $sin^2 θ_W = (3-φ)/6$. PDG 2024 lists the Z mass as 91187.6 ± 2.1 MeV. The upstream definition in ElectroweakMasses supplies the floating-point version 91187.6 for the same purpose.
proof idea
This is a direct one-line definition that assigns the integer constant 91188 to m_Z_exp with no tactics, lemmas or reductions applied.
why it matters
It supplies the experimental anchor for the wz_ratio_exp_comparison theorem and the z_relative_error bound inside the EWCert structure. The declaration supports verification that the Recognition Science Z prediction lies within 0.13 percent of experiment while keeping measured inputs outside the certified derivation chain. It touches the open separation between derived phi-ladder masses and imported PDG values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.