z_c_zero
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute z for any quark entry other than charm.
- Does not prove equality of observed and predicted masses for the general case.
- Does not address leptons or the full particle spectrum.
- Does not derive the underlying phi-ladder mass formula.
Lean usage
simp [chi2, quarksWitness, z_c_zero]formal statement (Lean)
72@[simp] lemma z_c_zero : z c_entry = 0 := by simp [z]