ILG_falsified
plain-language theorem explainer
ILG is falsified exactly when the median chi-squared per degree of freedom across the SPARC sample exceeds 5.0. Galaxy rotation-curve modelers testing zero-parameter phi-locked predictions cite this predicate to decide outright rejection of the ILG framework. The definition is a direct comparison against the constant generous_threshold.
Claim. The ILG model is falsified if the median $chi^2$/dof over the SPARC galaxy sample exceeds 5.0.
background
The SPARC falsifier module encodes the rejection test for ILG rotation-curve predictions under the zero per-galaxy free-parameter policy. All constants are locked to phi: alpha_t equals (1 minus 1/phi) over 2, C_lag equals phi to the minus 5, and Upsilon_star equals phi. The generous threshold is fixed at 5.0 to tolerate systematics, while the tight threshold of 3.0 directly tests the RS claim that the median chi2/dof should sit near 2.75.
proof idea
The definition is a one-line wrapper that applies the inequality generous_threshold < median_chi2_dof, where generous_threshold is the upstream constant 5.0.
why it matters
This predicate supplies the rejection criterion inside the SPARCFalsifierCert structure and the decidability theorem that splits every real input into falsified or passes. It closes the falsification protocol for the phi-locked ILG model against the SPARC sample, directly implementing the zero-free-parameter test required by the Recognition Science gravity sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.