def
definition
paper2_N_galaxies
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gravity.SPARCFalsifier on GitHub at line 116.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
113def paper2_mean_chi2 : ℝ := 4.23
114
115/-- Paper II SPARC Q=1 sample size. -/
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