ILG_passes
plain-language theorem explainer
ILG passes when the median chi-squared per degree of freedom across the SPARC sample is at most 5.0 under zero per-galaxy free parameters. Galaxy dynamics modelers cite this predicate when testing the phi-locked ILG rotation-curve formula against observations. The definition is a direct one-line comparison to the generous_threshold constant.
Claim. Let $m$ be the median of the chi-squared per degree of freedom values computed for the SPARC galaxies using the ILG formula with all parameters fixed by the Recognition Science constants. Then ILG passes if and only if $m ≤ 5$.
background
The SPARC Chi-Squared Falsifier module encodes the test for the ILG rotation-curve model: compute chi-squared per degree of freedom for each of the ~175 galaxies with zero free parameters per galaxy, take the median, and compare to a threshold. All parameters are locked to phi-derived values (alpha_t = (1 - 1/phi)/2, C_lag = phi^(-5), Upsilon_star = phi). generous_threshold is the constant 5.0 that permits systematic error while still allowing falsification if the median exceeds it.
proof idea
One-line definition that reduces directly to the inequality median_chi2_dof ≤ generous_threshold.
why it matters
ILG_passes supplies one disjunct in the decidability theorem falsification_decidable and appears inside the RS prediction statement H_SPARC_median and the certificate structure SPARCFalsifierCert. It implements the falsification protocol of the module (zero free parameters, phi-locked constants, median chi2/dof test) that sits inside the gravity section of the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.