module module moderate

`IndisputableMonolith.Gravity.SPARCFalsifier`

The Gravity.SPARCFalsifier module defines generous and tight chi-squared per dof thresholds plus decidability predicates to test falsification of the ILG model on SPARC galaxy data. It would be cited by researchers performing empirical checks of Recognition Science gravity predictions. The module consists entirely of definitions for thresholds, falsification flags, and parameter locks with no theorems or proofs.

claimIf the median value of $chi^2 / dof$ over the SPARC sample exceeds 5.0 then ILG is falsified; analogous conditions hold for the tight threshold and for the locked parameters $alpha$, $upsilon$, $clag$.

background

This module sits in the Gravity domain and imports IndisputableMonolith.Constants, whose sole documented object is the RS time quantum $tau_0 = 1$ tick. The supplied doc-comment states the generous falsification threshold for ILG chi-squared per dof: if median chi2/dof > 5.0 across the SPARC sample, ILG is falsified. Sibling declarations introduce the tight threshold, the predicate ILG_falsified, and the three locked-parameter conditions.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete falsification machinery for the ILG model inside the Recognition Science gravity section. It supports empirical testing of the phi-ladder mass and force predictions against rotation-curve data, thereby closing one observational loop in the T0-T8 forcing chain. No downstream theorems are recorded in the used_by edges.

scope and limits

Does not contain or process any SPARC data files.
Does not derive or prove the ILG force law.
Does not compute numerical chi-squared values.
Does not address falsifiers outside the SPARC chi-squared statistic.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (29)

def generous_threshold L45
def tight_threshold L50
def ILG_falsified L53
def RS_prediction_refuted L57
def ILG_passes L61
theorem falsification_decidable L65
def alpha_locked L73
def upsilon_locked L76
def clag_locked L79
theorem parameters_from_phi L82
def per_galaxy_free_parameters L90
theorem zero_free_params L92
def predicted_median L100
def H_SPARC_median L103
def paper2_median_chi2 L110
def paper2_mean_chi2 L113
def paper2_N_galaxies L116
def mond_median_chi2 L119
def mond_mean_chi2 L120
theorem ilg_better_mean_than_mond L124
structure GlobalOnlyPolicy L140
theorem global_only_policy L146
def NegativeControl L156
def velocity_permutation_control L159
def rotation_180_control L163
def gas_stars_swap_control L167
def all_controls_inflated L171
structure SPARCFalsifierCert L178
theorem sparc_falsifier_cert L186