acceptable_all_default_zero
plain-language theorem explainer
The lemma shows that the default PDG dataset meets the zero z and chi-squared thresholds for leptons, quarks, bosons, and baryons. PDG fit validators would cite it as the trivial baseline case. Its term proof decomposes the conjunction via direct application of the four species-specific zero-threshold lemmas after unfolding the default dataset.
Claim. Let $D$ denote the default dataset and let $T$ be the threshold pair with $zMax=0$ and $chi2Max=0$. Then $D$ satisfies the all-species acceptability predicate: acceptability holds for the lepton, quark, boson, and baryon sectors under $T$.
background
In the PDG.Fits module, the predicate acceptable_all aggregates four independent acceptability checks, one per particle sector, each comparing a species witness list against supplied zMax and chi2Max bounds. The defaultDataset supplies concrete witness lists for leptons, quarks, bosons, and baryons. Upstream lemmas acceptable_leptons, acceptable_quarks, acceptable_bosons, and acceptable_baryons each establish the zero-threshold case for their respective witnesses; the PrimitiveDistinction.from theorem supplies the seven-axiom foundation that justifies the structural conditions used in these checks.
proof idea
The proof is a term-mode refinement that introduces the four conjuncts of acceptable_all. Each conjunct is discharged by a simpa tactic that unfolds defaultDataset and invokes the matching species lemma (acceptable_leptons, acceptable_quarks, acceptable_bosons, acceptable_baryons).
why it matters
The declaration supplies the explicit baseline that the default dataset satisfies the (0,0) thresholds, matching its doc-comment. It anchors PDG fit constructions before any non-trivial threshold or mass-ladder analysis. Within the Recognition framework it closes the trivial case of the particle-data validation step that precedes application of the J-uniqueness or eight-tick octave structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.