H_SPARC_median
plain-language theorem explainer
The RS hypothesis asserts that an observed median chi-squared per degree of freedom for the SPARC sample lies within absolute distance 1.0 of the constant 2.75 while satisfying the ILG passage predicate. A researcher testing zero-parameter rotation-curve predictions against SPARC data would cite this as the quantitative benchmark for the Recognition Science median fit. The definition is a direct existential statement that combines the numerical tolerance interval with the ILG_passes condition.
Claim. There exists a real number $m$ such that $|m - 2.75| < 1$ and the ILG model passes for median chi-squared per degree of freedom equal to $m$.
background
The SPARC falsifier module encodes the test of the ILG rotation-curve model on the SPARC galaxy sample under zero per-galaxy free parameters. All constants are locked to phi-derived values: alpha_t = (1 - 1/phi)/2, C_lag = phi^{-5}, Upsilon_star = phi. The protocol computes chi-squared per degree of freedom for each galaxy and extracts the median across the sample. ILG_passes holds precisely when this median is at most the generous threshold. predicted_median is the constant 2.75, described in its doc-comment as the RS prediction for median chi2/dof within tolerance 1.0. The chi2 helper sums squared residuals over a list of species entries.
proof idea
The definition is a direct existential wrapper: it asserts the existence of an observed median within distance 1.0 of predicted_median while requiring that ILG_passes holds for that value. No lemmas are applied; the body simply unfolds the tolerance interval around the constant and conjoins the passage predicate.
why it matters
This definition supplies the concrete numerical benchmark (median chi2/dof ≈ 2.75 within 1.0) that anchors the falsification protocol in the module documentation. It closes the loop between the phi-locked parameters and the SPARC comparison, so that exceeding the threshold refutes the ILG model. The declaration therefore realizes the paper-II benchmark value cited at line ~3304 of the theory document and supplies the hypothesis that downstream falsification statements would invoke.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.