acceptable_all_mono
The lemma shows that acceptability of a full PDG dataset under Recognition Science thresholds is monotonic: tighter bounds imply looser bounds. A physicist tuning particle fits to the phi-ladder mass formula would cite it when relaxing zMax or chi2Max during iterative checks. The proof decomposes the four-way conjunction over leptons, quarks, bosons, and baryons then applies the single-list monotonicity lemma to each component.
claimLet $D$ be a dataset with lists of lepton, quark, boson, and baryon entries. Let $T_1, T_2$ be threshold pairs with $T_1.z_0 ≤ T_2.z_0$ and $T_1.χ^2_0 ≤ T_2.χ^2_0$. If each species list in $D$ satisfies the acceptability predicate at $T_1$, then each satisfies it at $T_2$.
background
In PDG.Fits a Dataset is the record holding four lists of SpeciesEntry (leptons, quarks, bosons, baryons). Thresholds is the record of real numbers zMax and chi2Max. The upstream definition acceptable_all D T asserts that the acceptable predicate holds simultaneously for all four lists at the supplied zMax and chi2Max values. The sibling lemma acceptable_mono states that for any single list, if z1 ≤ z2 and χ1 ≤ χ2 then acceptability at the tighter pair implies acceptability at the looser pair.
proof idea
Term-mode proof. Introduce the hypothesis that acceptable_all holds at T1, destructuring the conjunction into four separate facts. Apply acceptable_mono once to the leptons list, once to quarks, once to bosons, and once to baryons, supplying the same zMax and chi2Max inequalities in each case.
why it matters in Recognition Science
The lemma supplies the dataset-level monotonicity needed to justify threshold relaxation in PDG fits without rechecking every species. It directly supports the baseline claim that the default dataset meets the zero thresholds. Within Recognition Science it preserves compatibility of the phi-ladder assignments under progressive loosening of fit criteria, consistent with the eight-tick octave and the J-uniqueness fixed point.
scope and limits
- Does not prove that any concrete dataset meets the thresholds.
- Does not supply numerical values for zMax or chi2Max.
- Does not address the underlying mass formula or phi-ladder rung assignments.
- Does not extend monotonicity to datasets outside the PDG structure.
formal statement (Lean)
193lemma acceptable_all_mono (D : Dataset)
194 {T₁ T₂ : Thresholds}
195 (hZ : T₁.zMax ≤ T₂.zMax) (hC : T₁.chi2Max ≤ T₂.chi2Max) :
196 acceptable_all D T₁ → acceptable_all D T₂ := by
proof body
Term-mode proof.
197 intro h; rcases h with ⟨hl, hq, hb, hB⟩
198 refine And.intro ?hl' (And.intro ?hq' (And.intro ?hb' ?hB'))
199 · exact acceptable_mono (L:=D.leptons) hZ hC hl
200 · exact acceptable_mono (L:=D.quarks) hZ hC hq
201 · exact acceptable_mono (L:=D.bosons) hZ hC hb
202 · exact acceptable_mono (L:=D.baryons) hZ hC hB
203
204/-- Baseline: default dataset satisfies thresholds (0,0). -/