z_D0_zero
plain-language theorem explainer
The lemma establishes that the z-deviation for the Delta_0 species entry vanishes because its observed and predicted masses are identical. PDG mass-fit researchers cite it when assembling zero chi-squared results for the full baryon set and when verifying acceptability of the baryon witness. The proof is a direct simplification that unfolds the definition of z on this entry.
Claim. Let $z$ be the standardized residual function on species entries. For the Delta_0 entry with observed mass 1.232 GeV, uncertainty 0.005 GeV and predicted mass 1.232 GeV, $z$ evaluates to zero.
background
The PDG.Fits module defines SpeciesEntry as a record holding a particle name, observed mass, uncertainty sigma, and a predicted mass. The function z extracts the standardized difference between observed and predicted masses for a given entry. Delta_0_entry is the concrete record for the Delta_0 resonance in which the predicted mass is set exactly equal to the observed value 1.232. The lemma belongs to a family of zero-deviation statements for the six baryon species that together feed the chi-squared and acceptability calculations for the baryon witness.
proof idea
The proof is a one-line wrapper that invokes the simp tactic with the definition of z. Because the masses in Delta_0_entry coincide, the residual expression reduces immediately to zero.
why it matters
The result is invoked by chi2_baryons_zero to conclude that the total chi-squared over baryonsWitness is zero and by acceptable_baryons to discharge the zero-deviation case for this resonance. It supplies one concrete data point in the empirical check that Recognition Science mass predictions (via the phi-ladder) reproduce PDG values for the Delta resonances to within the stated uncertainties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.