all_controls_inflated
plain-language theorem explainer
Negative controls in the SPARC sample must produce higher chi-squared values than the ILG prediction under zero free parameters. This definition bundles the velocity permutation, 180-degree rotation, and gas-stars swap tests into one Prop for the falsification protocol. Researchers validating rotation-curve models with phi-locked constants would cite it when checking whether controls inflate chi2 above the ILG baseline. The definition is assembled as the direct conjunction of the three upstream control predicates.
Claim. The proposition that the chi-squared under velocity permutation exceeds the paper median, the chi-squared under 180-degree rotation exceeds the paper median, and the chi-squared under gas-stars swap exceeds the paper median.
background
The SPARC Chi-Squared Falsifier module formalizes the test for the ILG rotation-curve prediction on the SPARC galaxy sample. All parameters are locked to RS values derived from phi (alpha_t ≈ 0.191, C_lag = phi^{-5} ≈ 0.090, Upsilon_star = phi ≈ 1.618), with zero per-galaxy free parameters. Falsification occurs if the median chi2/dof across galaxies exceeds a chosen threshold (generous 5.0 or tight 3.0).
proof idea
This definition is a one-line wrapper that applies the conjunction of velocity_permutation_control, rotation_180_control, and gas_stars_swap_control. Each upstream predicate is defined as paper2_median_chi2 < chi2_xxx for its respective control.
why it matters
The definition packages the negative-control requirement that supports the overall falsification criterion for the ILG model. It directly implements the protocol step requiring controls to inflate chi2 above the ILG result, using the phi-derived constants listed in the module. It feeds the decidability and falsification predicates among the sibling declarations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.