chi2_quarks_zero
plain-language theorem explainer
The lemma establishes that the chi-squared statistic over the six quark species entries sums exactly to zero. Particle data analysts verifying Recognition Science mass fits would cite it to confirm zero residual in the quark sector. The proof is a direct simplification that unfolds the chi-squared sum and applies the individual z-zero lemmas for each quark entry.
Claim. Let $L$ be the list of quark species entries $[u, d, s, c, b, t]$. Define the chi-squared measure by $chi^2(L) = sum_{e in L} [z(e)]^2$. Then $chi^2(L) = 0$.
background
In the PDG.Fits module the chi2 definition folds the squared z values of each species entry into a single real number that quantifies total squared defect. The quarksWitness definition assembles the six standard quark entries into one list for sector-wide checks. Upstream lemmas z_u_zero through z_t_zero each establish that z vanishes on the corresponding entry by direct simplification against the z definition.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the chi2 definition, the quarksWitness list, and the six z-zero lemmas for the quark entries.
why it matters
The result is invoked by the acceptable_quarks lemma to discharge the chi-squared half of the acceptable predicate for the quark witness. It thereby closes the zero-defect verification for the quark sector, consistent with the Recognition Science phi-ladder mass formula where the six quarks sit at rungs yielding exact z = 0. No open scaffolding remains for this sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.