ILG_passes
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute or store the per-galaxy chi-squared values themselves.
- Does not enforce the tight threshold of 3.0 that matches the RS median prediction.
- Does not incorporate explicit modeling of systematic errors beyond the generous allowance.
- Does not depend on any particular implementation of the SPARC data set.
formal statement (Lean)
61def ILG_passes (median_chi2_dof : ℝ) : Prop :=
proof body
Definition body.
62 median_chi2_dof ≤ generous_threshold
63
64/-- The falsification criterion is decidable (for any real number). -/