def
definition
H_SPARC_median
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Gravity.SPARCFalsifier on GitHub at line 103.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
100def predicted_median : ℝ := 2.75
101
102/-- The RS prediction: median chi2/dof ≈ 2.75 (within 1.0). -/
103def H_SPARC_median : Prop :=
104 ∃ median_obs : ℝ, abs (median_obs - predicted_median) < 1.0 ∧
105 ILG_passes median_obs
106
107/-! ## Paper II Benchmark Values (Rotation-curves-Paper2-Sept-26.tex) -/
108
109/-- Paper II reports ILG median chi2/N = 2.75 on SPARC Q=1 subset. -/
110def paper2_median_chi2 : ℝ := 2.75
111
112/-- Paper II reports ILG mean chi2/N = 4.23 on SPARC Q=1 subset. -/
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