gas_stars_swap_control
plain-language theorem explainer
The gas-stars swap control requires that interchanging gas and stellar velocity contributions in SPARC galaxy fits yields a chi-squared per degree of freedom exceeding the ILG median of 2.75. Researchers validating zero-parameter rotation-curve models against empirical samples would cite this predicate when confirming negative controls. The definition reduces to a direct numerical comparison against the fixed benchmark supplied by Paper II.
Claim. Let $χ^2_{swap}$ be the chi-squared per degree of freedom obtained after interchanging the gas and stellar disk velocity fields. The control holds when $χ^2_{swap} > 2.75$, where 2.75 is the median value reported for the ILG model on the SPARC Q=1 subset.
background
The SPARC falsifier module encodes a zero-parameter test of the ILG rotation-curve prediction. All RS parameters are locked to phi: alpha_t = (1 - 1/phi)/2, C_lag = phi^{-5}, and Upsilon_star = phi. The protocol computes chi-squared per degree of freedom across the full SPARC sample and checks whether the median exceeds a threshold; Paper II supplies the benchmark median of 2.75 on the Q=1 subset. The chi-squared function is the sum of squared residuals over species entries.
proof idea
The definition is a one-line wrapper that applies the constant paper2_median_chi2 and checks the supplied swapped chi-squared value against it.
why it matters
This predicate is one of the three conjuncts inside all_controls_inflated, which certifies that every negative control inflates chi-squared above the ILG result. It therefore supports the overall falsification criterion for the ILG model on SPARC data with zero per-galaxy free parameters. The construction implements the module's protocol for testing phi-locked predictions against empirical rotation curves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.