def definition def or abbrev

`H_SPARC_median`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 103def H_SPARC_median : Prop :=

proof body

Definition body.

 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. -/

depends on (3)

Lean names referenced from this declaration's body.

ILG_passes in IndisputableMonolith.Gravity.SPARCFalsifier decl_use
predicted_median in IndisputableMonolith.Gravity.SPARCFalsifier decl_use
chi2 in IndisputableMonolith.PDG.Fits decl_use