NegativeControl
plain-language theorem explainer
NegativeControl defines a predicate on real numbers that encodes the negative control of randomly reassigning observed velocities to different radii in SPARC galaxy rotation curves. Researchers testing the ILG model with phi-locked parameters and zero free parameters per galaxy would cite this to verify that such shuffles drive chi-squared per degree of freedom well above the sample median. The declaration is a direct type definition to the real-to-proposition function space.
Claim. Let $N :$ $ℝ →$ Prop be the predicate that holds precisely when observed velocities have been randomly reassigned across different radii in the rotation curve data.
background
The module sets out the falsification protocol for the ILG rotation curve model on the SPARC sample of roughly 175 galaxies. All parameters are locked to values derived from phi, including alpha_t = (1 - 1/phi)/2, C_lag = phi^(-5), and Upsilon_star = phi, with zero per-galaxy free parameters allowed. The upstream abbrev Velocity := ℝ supplies the real numbers as the codomain for rotation velocities that enter the control predicate.
proof idea
The declaration is a direct definition that assigns the function type ℝ → Prop to the negative control concept, with the attached comment specifying the velocity permutation requirement.
why it matters
This definition supplies the type for the negative control test inside the SPARC falsification framework. It supports the module's protocol that computes median chi-squared per degree of freedom across the sample and declares the ILG model falsified when that median exceeds the chosen threshold (generous 5.0 or tight 3.0). The surrounding module references the theory document's claim of a median near 2.75 under the phi-derived parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.