Thresholds
plain-language theorem explainer
Thresholds packages two real bounds that set uniform acceptance criteria for z-scores and chi-squared statistics across particle species datasets. PDG fitters would cite it when applying the same cutoffs to leptons, quarks, bosons and baryons in a single call. The declaration is a bare structure definition carrying no proof obligations or computational content.
Claim. A record $T$ consisting of an upper bound $z_0$ on the z-statistic and an upper bound $c_0$ on the chi-squared statistic, used to test whether computed statistics for any species entry remain below the chosen limits.
background
The PDG.Fits module represents each particle species by a Dataset whose entries carry computed z and chi2 values. The predicate acceptable then returns true precisely when both statistics lie at or below supplied bounds. Thresholds bundles those two bounds into one record so the same pair can be passed to every species without repetition.
proof idea
Direct structure definition introducing the fields zMax and chi2Max of type real together with the deriving Repr instance. No lemmas or tactics are applied.
why it matters
Thresholds supplies the parameter type for acceptable_all, which conjoins the acceptability test over leptons, quarks, bosons and baryons, and for the monotonicity lemma acceptable_all_mono. It therefore parameterizes the statistical gate that decides whether a full PDG dataset is compatible with the Recognition Science mass-ladder predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.