paper2_median_chi2
plain-language theorem explainer
The definition records the median chi-squared per degree of freedom value of 2.75 reported for the ILG rotation curve model on the SPARC Q=1 subset. Galaxy dynamics researchers comparing zero-parameter predictions against observational data would reference this benchmark when evaluating control tests such as velocity permutations. The entry is supplied as a constant definition drawn from the cited paper.
Claim. The median value of $chi^2 / N$ for the ILG model fitted to the SPARC galaxy sample with zero free parameters is $2.75$.
background
SPARC denotes the sample of spiral galaxies with high-quality rotation curve data. ILG is the Indisputable Logic Gravity model whose parameters (alpha_t, C_lag, Upsilon_star) are locked to the golden ratio phi with no per-galaxy adjustments. The chi-squared statistic sums squared residuals between observed and predicted velocities, normalized per degree of freedom, as defined upstream by the sum-of-squares function on a list of species entries.
proof idea
The definition is a direct numerical assignment of the constant 2.75 taken from the external paper report. No lemmas are applied; it serves as a reference value for subsequent control comparisons.
why it matters
This constant anchors the falsification tests in the SPARC module. It is used by the gas-stars swap, rotation 180, and velocity permutation controls to verify that any deviation inflates the chi-squared above the reported ILG median. The entry implements the specific RS prediction of median chi2/dof ~2.75 under phi-locked parameters, closing the loop from the forcing chain to observable galaxy dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.