mond_median_chi2

formal source

 116def paper2_N_galaxies : ℕ := 127
 117
 118/-- MOND simple-nu comparison: median 2.47, mean 4.65. -/
 119def mond_median_chi2 : ℝ := 2.47
 120def mond_mean_chi2 : ℝ := 4.65
 121
 122/-- ILG has higher median but LOWER mean than MOND — it handles
 123    outliers better due to the global-only constraint. -/
 124theorem ilg_better_mean_than_mond :
 125    paper2_mean_chi2 < mond_mean_chi2 := by
 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. -/
 140structure GlobalOnlyPolicy where
 141  alpha_from_phi : alpha_locked = (1 - 1/phi) / 2
 142  upsilon_from_phi : upsilon_locked = phi
 143  clag_from_phi : clag_locked = phi ^ (-(5 : ℝ))
 144  per_galaxy_params : per_galaxy_free_parameters = 0
 145
 146theorem global_only_policy : GlobalOnlyPolicy where
 147  alpha_from_phi := parameters_from_phi.1
 148  upsilon_from_phi := parameters_from_phi.2.1
 149  clag_from_phi := parameters_from_phi.2.2