predicted_median
plain-language theorem explainer
The definition records the Recognition Science benchmark value of 2.75 for the median chi-squared per degree of freedom in zero-free-parameter ILG fits to the full SPARC galaxy sample. Galaxy-dynamics groups applying the falsification protocol would cite this constant when comparing an observed median against the RS target. It is supplied by a direct numeric assignment that matches the claim in the module documentation.
Claim. The RS-predicted median of $chi^2 / dof$ for the ILG model across the SPARC sample equals $2.75$.
background
The SPARC Chi-Squared Falsifier module encodes a test for the ILG rotation-curve model with all parameters locked to phi-derived constants: alpha_t = (1 - 1/phi)/2, C_lag = phi^{-5}, Upsilon_star = phi. The falsification protocol computes chi2/dof for each of the ~175 galaxies using zero per-galaxy free parameters, then takes the median. The upstream chi2 definition from PDG.Fits is the sum of squared residuals: def chi2 (L : List SpeciesEntry) : ℝ := L.foldl (fun acc e => acc + (z e) * (z e)) 0. Module documentation states that the theory document claims median chi2/dof ~ 2.75.
proof idea
This is a one-line definition that directly assigns the constant 2.75.
why it matters
The value supplies the target for the downstream H_SPARC_median hypothesis, which requires an observed median within 1.0 of 2.75 together with ILG_passes. It implements the specific RS prediction cited in the module's falsification protocol and the rotation-curves paper. In the Recognition framework it anchors the empirical test of the phi-locked parameters in the gravity sector of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.