SPARC_mismatch_falsifier
plain-language theorem explainer
The SPARC mismatch falsifier encodes the rejection criterion for the ILG global rotation model against the SPARC galaxy sample. Researchers fitting rotation curves with fixed M/L equal to phi and locked alpha would cite this threshold to test the framework. The definition is a direct one-line inequality on the supplied chi-squared value.
Claim. The proposition holds precisely when the reduced chi-squared statistic for the ILG-predicted rotation curves (with mass-to-light ratio $M/L = ϕ$ and coupling locked at $α_{lock}$) exceeds 2.0 against the SPARC database.
background
Recognition Science models galactic dynamics via the J-cost functional and phi-ladder mass assignments. The ILG global-only fit fixes the mass-to-light ratio at the golden ratio phi and locks the fine-structure parameter alpha to its Recognition value derived from the eight-tick octave and spectral emergence. SPARC supplies a uniform set of high-resolution rotation curves for direct comparison.
proof idea
The definition is a direct one-line encoding of the inequality chi_sq > 2.0. No lemmas or tactics are invoked; the body simply returns the Prop that the input real exceeds the conventional threshold of 2.0 for acceptable fit quality.
why it matters
This definition supplies the concrete falsification test for the ILG rotation model inside the Gravity module. It operationalizes the claim that a global-only fit with M/L = phi and alpha_lock must reproduce SPARC data or the Recognition framework is refuted. The threshold closes the loop from the phi-forcing chain (T5 J-uniqueness through T8 D=3) to observable predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.