def
definition
predicted_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 100.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
97These are encoded as hypotheses (to be discharged by the Python script). -/
98
99/-- RS-predicted median chi2/dof across SPARC. -/
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