ilg_better_mean_than_mond
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.