velocity_permutation_control
plain-language theorem explainer
The definition encodes the velocity permutation negative control for the ILG rotation-curve falsifier on SPARC data, requiring that randomly reassigning observed velocities to different radii produces a chi-squared per degree of freedom strictly larger than the Paper II median of 2.75. Galaxy-dynamics researchers testing zero-parameter models would cite it to confirm that the ILG prediction beats this randomization baseline. The definition is a direct inequality against the fixed median constant.
Claim. Let $2.75$ be the median chi-squared per degree of freedom reported for the ILG model on the SPARC Q=1 sample. The velocity-permutation control holds precisely when a chi-squared value obtained by randomly reassigning observed velocities to different radii satisfies $2.75 < chi2_perm$.
background
The SPARC falsifier module implements a zero-free-parameter test of the ILG rotation-curve prediction on the SPARC galaxy sample. All parameters are locked to Recognition-Science values derived from phi: alpha_t = (1 - 1/phi)/2, C_lag = phi^{-5}, and Upsilon_star = phi. The velocity permutation acts as one of three negative controls that must inflate chi-squared if the ILG fit is physically meaningful rather than accidental.
proof idea
One-line definition that applies the inequality paper2_median_chi2 < chi2_perm, where paper2_median_chi2 is the constant 2.75 taken directly from the upstream definition reporting the Paper II median on the SPARC Q=1 subset.
why it matters
This definition is required by the downstream all_controls_inflated predicate, which demands that velocity permutation, 180-degree rotation, and gas-stars swap all produce chi-squared values above the ILG result. It thereby supports the module's falsification protocol: if the median chi2/dof across SPARC exceeds the chosen threshold under zero per-galaxy parameters, the ILG model is refuted. The construction closes one concrete negative-control slot in the SPARC test for phi-locked gravity predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.