z_d_zero
plain-language theorem explainer
The lemma shows that the standardized residual z for the down quark entry is exactly zero. Physicists fitting PDG quark masses would reference it to confirm exact agreement between prediction and observation for the d quark. The proof reduces immediately via simplification of the z definition.
Claim. For the down quark species entry with observed mass 0.0047, uncertainty 0.0010 and predicted mass 0.0047, the standardized residual satisfies $z = 0$.
background
The PDG.Fits module defines SpeciesEntry as a structure with name, observed mass, sigma, and predicted mass. The z function is the standardized residual (observed minus predicted) divided by sigma. This lemma depends on the d_entry definition which sets the observed and predicted masses equal for the down quark. It is one of several zero-residual lemmas for quarks.
proof idea
The proof is a one-line wrapper that applies the simp tactic using the definition of z. The equality holds immediately because observed and predicted masses match in the down quark entry.
why it matters
This lemma is invoked by chi2_quarks_zero to show the quark chi-squared is zero and by acceptable_quarks to verify the fit. It confirms that Recognition Science phi-ladder predictions match PDG data for the down quark. This supports the mass formula yardstick times phi to a power on the ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.