acceptable_mono
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not define the internal form of the acceptability predicate.
- Does not treat multi-list or full-dataset acceptability.
- Does not incorporate Recognition Science constants such as phi or J-cost.
- Does not establish existence of acceptable thresholds for given data.
formal statement (Lean)
182lemma acceptable_mono {L : List SpeciesEntry}
183 {z₁ z₂ χ₁ χ₂ : ℝ}
184 (hz : z₁ ≤ z₂) (hχ : χ₁ ≤ χ₂) :
185 acceptable L z₁ χ₁ → acceptable L z₂ χ₂ := by
proof body
Term-mode proof.
186 intro h
187 rcases h with ⟨hzs, hchi⟩
188 refine And.intro ?hzs' ?hchi'
189 · intro e he; exact le_trans (hzs e he) hz
190 · exact le_trans hchi hχ
191
192/-- Monotonicity of all-species acceptability in the thresholds. -/