quarksWitness
plain-language theorem explainer
This definition assembles the six quark flavor entries from PDG data into a single list of SpeciesEntry structures. Researchers fitting particle masses in the Recognition Science framework cite it when building the default dataset or verifying zero chi-squared results for the quark sector. The implementation is a direct list literal that enumerates the pre-defined up, down, strange, charm, bottom, and top entries.
Claim. Let $W_q$ be the list of SpeciesEntry records for the six quarks, consisting of the up, down, strange, charm, bottom, and top entries, where each record holds a name string together with observed mass, uncertainty, and predicted mass in the reals.
background
In the PDG.Fits module, SpeciesEntry is the structure with fields name (String), mass_obs (ℝ), sigma (ℝ), and mass_pred (ℝ). The module supplies concrete data for testing Recognition Science mass predictions against experiment. Each quark entry sets mass_obs equal to mass_pred using PDG central values, with the listed uncertainties. Upstream definitions supply the individual entries b_entry, c_entry, d_entry, s_entry, and t_entry (plus the missing u_entry) as explicit records with matching observed and predicted masses.
proof idea
The declaration is a definition by direct list construction that enumerates the six quark entries. No lemmas or tactics are invoked; the body is simply the list literal referencing the sibling entry definitions.
why it matters
The list is consumed by acceptable_quarks to establish that every entry satisfies the zero-defect acceptance predicate, by chi2_quarks_zero to prove the quark-sector chi-squared statistic equals zero, and by defaultDataset to populate the full particle collection. It therefore supplies the quark-sector input required for the PDG fits that check the Recognition Science mass formula against data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.