acceptable_mono
plain-language theorem explainer
Acceptability of a species list is monotonic in the z and chi thresholds: raising them preserves the property. PDG researchers fitting particle masses cite this when adjusting fit criteria. The proof extracts the component bounds and applies order transitivity to each.
Claim. Let $L$ be a list of species entries. For real numbers $z_1, z_2, χ_1, χ_2$ with $z_1 ≤ z_2$ and $χ_1 ≤ χ_2$, if $L$ meets the acceptability conditions at thresholds $(z_1, χ_1)$ then it meets them at $(z_2, χ_2)$.
background
In the PDG.Fits module a SpeciesEntry records a particle name, observed mass, uncertainty sigma and predicted mass. The acceptability predicate on list $L$ at thresholds $z$ and $χ$ holds precisely when every entry satisfies a z-score bound by $z$ and the aggregate chi-squared is bounded by $χ$. The lemma sits inside the PDG fits layer that compares predicted lepton masses against observation.
proof idea
The term proof introduces the acceptability hypothesis, cases it into the z-score and chi-squared conjuncts, then builds the target conjunction by applying le_trans from ArithmeticFromLogic to the z-scores under the raised threshold and chaining the chi-squared inequality directly.
why it matters
The result is invoked by acceptable_all_mono to lift monotonicity to full datasets. It supplies the basic threshold-relaxation step required for systematic PDG fits in Recognition Science, where stable acceptance criteria support comparison of predicted spectra to observed particle data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.