ILG_passes
plain-language theorem explainer
ILG passes the falsification test when the median chi-squared per degree of freedom across the SPARC galaxy sample is at most 5.0. Rotation-curve analysts would cite this predicate when verifying that the phi-locked ILG model survives the empirical benchmark with zero per-galaxy free parameters. The definition reduces directly to an inequality against the constant generous_threshold.
Claim. Let $m$ be the median of the per-galaxy values of chi-squared per degree of freedom computed on the SPARC sample under the ILG rotation-curve model with all parameters fixed by phi. Then ILG passes when $m$ satisfies $m$ ≤ 5.
background
The SPARC Falsifier module encodes an empirical test for the ILG rotation-curve prediction inside Recognition Science. All galaxy-specific parameters are locked to phi-derived constants: alpha_t = (1 - 1/phi)/2, C_lag = phi^(-5), and Upsilon_star = phi. The protocol generates predicted rotation curves for the full SPARC sample using zero free parameters per galaxy, evaluates chi-squared per degree of freedom for each object, and extracts the median of those values.
proof idea
The definition is a one-line wrapper that applies the inequality median_chi2_dof ≤ generous_threshold, where generous_threshold expands to the literal constant 5.0.
why it matters
This predicate supplies the positive branch of the decidable falsification criterion consumed by falsification_decidable, H_SPARC_median, and SPARCFalsifierCert. It directly implements the falsification protocol in the module documentation, which declares ILG falsified only when the median exceeds the threshold. The construction closes the empirical loop for the gravity sector by furnishing a concrete, decidable test against SPARC data under the zero-parameter constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.