falsification_decidable
falsification_decidable establishes that for any real median chi-squared per degree of freedom the ILG model is either falsified or passes the generous threshold. Researchers auditing the SPARC rotation-curve test in the Recognition Science gravity module would cite it to confirm the criterion is decidable. The proof is a one-line term that unfolds the threshold definitions and splits on the ordering le_or_gt.
claimFor any real number $x$, either $x > 5$ (ILG falsified) or $x ≤ 5$ (ILG passes).
background
The SPARC Chi-Squared Falsifier module formalizes a test for the ILG rotation-curve prediction under zero per-galaxy free parameters. ILG_falsified holds when the median chi-squared per degree of freedom exceeds the generous threshold of 5.0; ILG_passes holds when the median is at most 5.0. The module locks RS parameters to phi-derived values (alphaLock = (1 − 1/phi)/2, C_lag = phi^−5, Upsilon_star = phi) and requires the median to be computed across the full SPARC sample before applying the threshold.
proof idea
The term proof unfolds ILG_falsified, ILG_passes and generous_threshold (which is the constant 5.0), then applies le_or_gt x 5.0 and routes the two branches of the ordering into the respective disjuncts via elim.
why it matters in Recognition Science
The result supplies the decidability witness required by sparc_falsifier_cert, which assembles the full SPARCFalsifierCert record containing zero_free_params, parameters_from_phi and the global-only policy. It closes the falsification protocol step that compares the median chi2/dof against the generous threshold of 5.0 while the tight threshold of 3.0 remains available for the stricter RS prediction test.
scope and limits
- Does not compute any chi-squared values from SPARC data.
- Does not invoke the tight threshold of 3.0.
- Does not admit per-galaxy free parameters.
- Applies exclusively to the generous threshold constant 5.0.
formal statement (Lean)
65theorem falsification_decidable (x : ℝ) :
66 ILG_falsified x ∨ ILG_passes x := by
proof body
Term-mode proof.
67 unfold ILG_falsified ILG_passes generous_threshold
68 exact le_or_gt x 5.0 |>.elim (Or.inr) (Or.inl)
69
70/-! ## RS Parameter Lock -/
71
72/-- The alpha parameter is locked to alphaLock ≈ 0.191. -/