RS_prediction_refuted
plain-language theorem explainer
The declaration defines the condition under which the Recognition Science rotation curve prediction is refuted by SPARC data. A physicist testing the zero-free-parameter ILG model would cite this to decide if the phi-locked forecast fails. It is implemented as a direct inequality comparison of the observed median chi-squared per degree of freedom against the constant tight_threshold of 3.0.
Claim. The RS prediction is refuted when the median chi-squared per degree of freedom across the SPARC galaxy sample exceeds 3.0, i.e., when median($chi^2$/dof) > 3.0 with all parameters locked to $phi$.
background
The module formalizes the falsification criterion for the ILG rotation curve prediction: compute ILG curves for the ~175 SPARC galaxies using zero per-galaxy free parameters, form chi-squared per degree of freedom for each, take the median, and compare against a threshold. The tight_threshold is defined as 3.0 to test the specific RS prediction (claimed median ~2.75). Upstream results supply the tight_threshold constant and ensure the empirical program remains collision-free and algebraically closed.
proof idea
One-line definition that applies the inequality tight_threshold < median_chi2_dof, directly encoding the falsification condition stated in the module doc-comment.
why it matters
This definition supplies the precise trigger for refuting the RS-specific ILG prediction inside the Recognition Science gravity module. It supports sibling declarations such as ILG_falsified and falsification_decidable. The threshold choice directly tests the phi-locked parameters (alpha_t, C_lag, Upsilon_star) that descend from the eight-tick octave and phi-ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.