z_Z_zero
plain-language theorem explainer
The lemma establishes that the deviation measure z applied to the Z boson species entry equals zero, since its observed and predicted masses are identical. PDG data fitters cite this result when confirming that the Z contributes no residual to boson chi-squared sums. The proof reduces immediately by simplification on the definition of z.
Claim. Let $Z_0$ be the species entry with observed mass 91.1876 GeV, uncertainty 0.0021 GeV, and predicted mass 91.1876 GeV. Then the normalized residual $z(Z_0) = 0$.
background
The PDG.Fits module records particle data via the SpeciesEntry structure, which stores a name, observed mass, sigma, and predicted mass. The function z computes the normalized residual (observed minus predicted, scaled by sigma) for any such entry. This lemma depends only on the concrete definition of the Z entry, whose masses match exactly.
proof idea
One-line simp wrapper that unfolds the definition of z and cancels the identical mass terms.
why it matters
The result is invoked by chi2_bosons_zero to obtain a total boson chi-squared of zero and by acceptable_bosons to certify fit acceptability. It closes the exact-prediction case for the Z boson inside the PDG fits layer of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.