acceptable
plain-language theorem explainer
The acceptable predicate certifies that every standardized residual in a list of particle species entries stays within a chosen bound while the aggregate chi-squared sum remains below its threshold. Researchers fitting Recognition Science mass predictions to PDG central values invoke it to certify agreement for leptons, quarks, bosons, and baryons. The definition is a direct conjunction of the per-entry bound and the chi-squared comparison, with no reduction or lemmas required.
Claim. A list $L$ of species entries is acceptable at thresholds $z_0$ and $C_0$ when $|z(e)|$ is at most $z_0$ for every entry $e$ in $L$ and the sum of squared residuals over $L$ is at most $C_0$.
background
The PDG.Fits module represents particle data as lists of SpeciesEntry records, each holding a name, observed mass, uncertainty sigma, and a predicted mass. The companion chi2 function returns the sum of squared standardized residuals across such a list. This supplies the acceptance test for comparing Recognition Science mass predictions, derived from the phi-ladder with rung and gap corrections, against PDG 2024 central values.
proof idea
The definition is a primitive conjunction. Its first conjunct asserts that the absolute standardized residual of every entry in the input list is bounded by zMax. Its second conjunct asserts that the chi2 value of the list, obtained by folding the sum of squared residuals, does not exceed chi2Max. No lemmas are applied.
why it matters
This predicate is the common interface called by the lemmas acceptable_leptons, acceptable_quarks, acceptable_bosons, and acceptable_baryons, each establishing the condition at zero thresholds for the corresponding witness list. It also supports acceptable_all over the full dataset and the monotonicity result acceptable_mono. In the Recognition framework it supplies the quantitative check that the forced constants (T5 J-uniqueness, T6 phi fixed point, T8 D=3) reproduce the observed spectrum to within experimental precision.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.