`zero_free_params`

proved

show as: view math explainer →

module: IndisputableMonolith.Gravity.SPARCFalsifier
domain: Gravity
line: 92 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gravity.SPARCFalsifier on GitHub at line 92.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  89/-- The number of per-galaxy free parameters is exactly zero. -/
  90def per_galaxy_free_parameters : ℕ := 0
  91
  92theorem zero_free_params : per_galaxy_free_parameters = 0 := rfl
  93
  94/-! ## SPARC Benchmark Values
  95
  96The theory document (line ~3304) gives benchmark chi2 values.
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.