all_controls_inflated
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute numerical chi-squared values from data.
- Does not select or apply any specific threshold value.
- Does not include the ILG rotation-curve prediction itself.
- Does not address the median operation across the galaxy sample.
formal statement (Lean)
171def all_controls_inflated (chi2_perm chi2_rot chi2_swap : ℝ) : Prop :=
proof body
Definition body.
172 velocity_permutation_control chi2_perm ∧
173 rotation_180_control chi2_rot ∧
174 gas_stars_swap_control chi2_swap
175
176/-! ## Certificate -/
177