z_Dm_zero
plain-language theorem explainer
The lemma establishes that z evaluates to zero on the Delta_m species entry. PDG mass fit verifications cite it to confirm exact agreement between predicted and observed masses for the Delta resonance. The one-line simp proof reduces immediately from the equality of mass_obs and mass_pred in the entry definition.
Claim. $z(Delta_m) = 0$, where $Delta_m$ is the SpeciesEntry with observed mass 1.232 GeV, predicted mass 1.232 GeV, and sigma 0.005 for the Delta^- baryon.
background
The PDG.Fits module defines SpeciesEntry structures that pair observed masses from the Particle Data Group with model predictions. The z function computes the standardized residual for each entry. Delta_m_entry is the specific definition for the Delta(1232) resonance with matching masses at 1.232 GeV. This lemma belongs to the suite of zero-residual results for baryons.
proof idea
This is a one-line wrapper that applies the simp tactic to the definition of z, which immediately yields zero given the identical mass_obs and mass_pred fields in Delta_m_entry.
why it matters
The lemma supports chi2_baryons_zero by supplying the zero residual for Delta_m, which combines with results for other baryons to yield overall chi-squared of zero. It also aids acceptable_baryons in verifying the witness. Within the Recognition framework this contributes to demonstrating exact fits for baryon masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.