acceptable_all
plain-language theorem explainer
The definition acceptable_all asserts that a Dataset of particle species satisfies the acceptability predicate simultaneously on its leptons, quarks, bosons and baryons lists at supplied zMax and chi2Max thresholds. PDG data analysts checking Recognition Science fits would cite this predicate to enforce uniform multi-sector consistency. It is realized as an explicit four-way conjunction of the single-sector acceptable predicate.
Claim. Let $D$ be a dataset whose fields are lists of species entries for leptons, quarks, bosons and baryons, and let $T$ be a threshold pair $(z_ {max}, chi^2_{max})$. Then acceptable_all$(D,T)$ holds if and only if each of the four lists satisfies the single-sector acceptability condition at those thresholds.
background
In the PDG.Fits module a Dataset is the structure carrying four parallel lists of SpeciesEntry (leptons, quarks, bosons, baryons). Thresholds is the companion structure holding the two real bounds zMax and chi2Max that control deviation tolerances. The definition sits directly above the sibling predicate acceptable, which is applied once to each list.
proof idea
The definition is a direct structural conjunction that applies the acceptable predicate to D.leptons, D.quarks, D.bosons and D.baryons, each time passing the common T.zMax and T.chi2Max. No lemmas or tactics are required; it is a one-line wrapper that unfolds the four sector checks.
why it matters
acceptable_all supplies the joint predicate consumed by the monotonicity lemma acceptable_all_mono and the baseline lemma acceptable_all_default_zero. It completes the uniform-threshold verification step required for PDG fits, ensuring that the three-generation structure forced by SpectralEmergence remains consistent with empirical data across all sectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.