z_Dp_zero
plain-language theorem explainer
The lemma shows that the standardized residual z applied to the Delta_p species entry equals zero because its observed mass of 1.232 exactly matches the predicted mass. Researchers fitting baryon masses in the PDG module of Recognition Science cite this to confirm zero contribution from this particle to chi-squared totals. The proof is a direct simplification that unfolds the definition of z on the given entry.
Claim. Let $e$ be the species entry for the Delta_p baryon with observed mass 1.232, uncertainty 0.005 and predicted mass 1.232. Then the standardized residual function satisfies $z(e)=0$.
background
In the PDG.Fits module species entries store observed mass, uncertainty and predicted mass for each particle. The function z computes the standardized residual (observed minus predicted) divided by sigma for any such entry. Delta_p_entry is the concrete record for the Delta^+ baryon whose observed and predicted masses are set equal at 1.232. This zero-residual lemma belongs to the family of baryon results that also includes the proton, neutron and other Delta states; it is invoked directly by the chi-squared summation over the baryon witness set.
proof idea
The proof is a one-line wrapper that applies the simp tactic with the definition of z, which immediately reduces the equality to the numerical identity 1.232 - 1.232 = 0.
why it matters
This result is used by chi2_baryons_zero to establish that the total chi-squared over the baryon witness is zero and by acceptable_baryons to verify the acceptability predicate. It therefore supports the exact match between Recognition Science mass predictions and PDG data for the listed baryons. Within the framework the lemma closes one of the zero-deviation cases required for the overall baryon fit to be acceptable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.