acceptable_quarks
plain-language theorem explainer
The lemma establishes that the quark witness list satisfies the zero-threshold acceptance condition, with all mass deviations exactly zero and the chi-squared statistic vanishing. Particle data analysts checking Recognition Science predictions against PDG 2024 values would cite it to confirm baseline consistency for the six quark flavors. The proof relies on exhaustive case analysis over the witness entries combined with direct application of the per-flavor zero lemmas and the chi-squared zero lemma.
Claim. Let $W$ be the list of six quark species entries with predicted masses set equal to observed PDG central values. Then every entry $e$ in $W$ satisfies $|z(e)| = 0$ and the chi-squared statistic satisfies $chi^2(W) = 0$.
background
The acceptance predicate on a list of species entries requires that the absolute normalized deviation |z| for each entry stays at most zMax and that the overall chi-squared value stays at most chi2Max. The quarksWitness assembles the six entries for up, down, strange, charm, bottom and top quarks, each with mass_pred set exactly to the observed mass_obs so that individual z values are zero. This lemma belongs to the PDG fits module that supplies default witnesses for testing the Recognition Science mass predictions against experimental data. It builds on the general acceptable definition together with the dedicated zero lemmas for each quark flavor and the chi-squared vanishing result for the full quark list.
proof idea
The proof splits the conjunction into the universal property over entries and the chi-squared bound. For the universal property it introduces an arbitrary entry, derives the six possible cases from the definition of the witness list, and substitutes each case to apply the corresponding zero-deviation lemma. The chi-squared bound is obtained immediately by simplification from the chi-squared zero lemma.
why it matters
This lemma supplies the quark component of the baseline result acceptable_all_default_zero, which verifies that the complete default dataset meets the zero thresholds. It thereby certifies exact reproduction of PDG central values by the Recognition Science phi-ladder mass formula for quarks, forming part of the auditable zero-chi-squared witnesses before introducing gaps or uncertainties in the mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.