z_c_zero
plain-language theorem explainer
The lemma establishes that the standardized residual for the charm quark entry is exactly zero. Researchers assembling chi-squared fits of PDG quark masses to Recognition Science predictions would cite this when confirming zero contribution from matched entries. The proof is a direct simplification that reduces via the definition of z.
Claim. Let $z$ be the standardized residual function on a SpeciesEntry. Then $z(c) = 0$, where $c$ is the charm quark entry with observed mass 1.27 and predicted mass 1.27.
background
The PDG.Fits module defines SpeciesEntry as a record holding particle name, observed mass, sigma uncertainty, and predicted mass. The function z computes the standardized residual for any such entry. The charm entry is supplied as a concrete datum with identical observed and predicted masses. This sits inside the broader PDG fitting layer that compares observed values against phi-ladder predictions from the Recognition Science mass formula.
proof idea
One-line wrapper that applies the simp tactic to the definition of z. The tactic immediately reduces the expression to zero because the observed and predicted masses in the charm entry are identical.
why it matters
The result is invoked inside chi2_quarks_zero to obtain total chi-squared zero for the quark sector and inside acceptable_quarks to verify the acceptance predicate at zero deviation. It therefore supports the exact match of the charm datum to the Recognition Science prediction on the phi-ladder. No open scaffolding questions are closed by this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.