falsification_decidable
plain-language theorem explainer
The theorem states that for any real number x representing median chi-squared per degree of freedom, either the ILG model is falsified by exceeding the generous threshold or it passes the test. Empirical gravity modelers testing Recognition Science predictions against SPARC data would cite this when establishing decidability of the falsification criterion. The proof is a one-line term-mode reduction that unfolds the threshold definitions and applies the real ordering lemma le_or_gt.
Claim. For any real number $x$, either $5 < x$ (ILG falsified) or $x ≤ 5$ (ILG passes).
background
The module formalizes a chi-squared falsifier for the ILG rotation-curve model on the SPARC sample under zero per-galaxy free parameters. ILG_falsified(x) holds when the generous threshold 5.0 is exceeded by the median chi2/dof; ILG_passes(x) holds when the median is at most 5.0. The generous_threshold definition supplies the concrete cutoff 5.0, while upstream constants such as alphaLock = (1 − 1/φ)/2 lock the RS parameters used in the broader ILG prediction.
proof idea
The term proof unfolds ILG_falsified, ILG_passes and generous_threshold, then invokes le_or_gt x 5.0 and eliminates the resulting disjunction into the two constructors.
why it matters
The result supplies the criterion_decidable field of sparc_falsifier_cert, which certifies that the SPARC test uses zero free parameters, parameters drawn from phi, and a decidable falsification rule. It directly implements the falsification protocol described in the module (median chi2/dof compared to the generous threshold of 5.0) and closes the decidability step required for the empirical claim in the Recognition Science gravity section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.