ilg_better_mean_than_mond
ILG yields a strictly lower mean chi-squared per degree of freedom than MOND across the full SPARC sample. Galaxy rotation-curve modelers comparing zero-parameter predictions would cite the result when arguing that global-only constraints improve outlier robustness. The proof is a one-line wrapper that unfolds the two mean definitions and reduces the inequality by direct numeric evaluation.
claimLet $m_{ILG}$ be the mean chi-squared per degree of freedom for the ILG rotation-curve predictions and $m_{MOND}$ the corresponding mean for MOND. Then $m_{ILG} < m_{MOND}$.
background
The module formalizes a falsification test for ILG rotation curves on the SPARC catalog. All model parameters are locked to Recognition Science constants derived from phi: alpha_t = (1 - 1/phi)/2, C_lag = phi^{-5}, Upsilon_star = phi. The global-only policy requires that the weight function w(r) depend solely on these catalog-level constants and the photometric baryonic profile; no kinematic data or per-galaxy parameters enter the prediction. Upstream results supply the phi-forcing structure (PhiForcingDerived.of), the fine-structure constant (Constants.Alpha.alpha), and the ledger factorization that calibrates J-cost.
proof idea
The proof is a one-line wrapper. It unfolds the definitions of paper2_mean_chi2 and mond_mean_chi2, then applies norm_num to discharge the resulting numeric inequality.
why it matters in Recognition Science
The theorem supplies the ilg_beats_mond_mean field inside the SPARC falsifier certificate (sparc_falsifier_cert). That certificate collects zero_free_params, parameters_from_phi, and the global-only policy to certify that ILG survives the median-chi2 test with no free parameters. The result therefore closes one link in the chain from phi-locked constants to an empirical falsification criterion for the ILG model.
scope and limits
- Does not claim ILG has lower median chi-squared than MOND.
- Does not apply to any single galaxy; only to the sample-wide mean.
- Does not incorporate per-galaxy free parameters or kinematic fitting.
- Does not address systematic errors beyond the stated generous threshold.
Lean usage
theorem sparc_falsifier_cert : SPARCFalsifierCert where ... ilg_beats_mond_mean := ilg_better_mean_than_mondformal statement (Lean)
124theorem ilg_better_mean_than_mond :
125 paper2_mean_chi2 < mond_mean_chi2 := by
proof body
Term-mode proof.
126 unfold paper2_mean_chi2 mond_mean_chi2; norm_num
127
128/-! ## Global-Only Policy (Paper I + Paper II) -/
129
130/-- The global-only policy: the ILG weight function w(r) depends ONLY
131 on catalog-level constants (alpha, C_lag, Upsilon, tau_star) and
132 the photometric baryonic profile (v_gas, v_disk, v_bul).
133
134 It does NOT depend on:
135 - The observed rotation velocity (kinematic data)
136 - Any per-galaxy fitted parameter
137 - The galaxy's morphological classification (beyond photometry)
138
139 This is formalized as: the parameters are functions of phi alone. -/