module module high

`IndisputableMonolith.Gravity.SPARCFalsifier`

The Gravity.SPARCFalsifier module defines numerical thresholds and boolean predicates for falsifying the ILG model against SPARC galaxy rotation-curve data via median chi-squared per degree of freedom. A physicist testing Recognition Science gravity predictions against observations would cite these constants and predicates when evaluating model viability. The module consists of imported constants from the RS time quantum together with simple threshold definitions and no deductive proofs.

claimGenerous threshold: if median $chi^2/mathrm{dof} > 5.0$ across the SPARC sample then ILG is falsified. Tight threshold and predicates ILG_falsified, RS_prediction_refuted, ILG_passes are likewise defined as decidable conditions on the same sample.

background

Recognition Science derives gravity from the T0-T8 forcing chain that fixes D=3 spatial dimensions and phi-based constants in RS-native units. The SPARCFalsifier module sits inside the gravity domain and imports the fundamental RS time quantum tau_0 = 1 tick from Constants. It introduces chi-squared per degree of freedom thresholds applied to fits of the SPARC sample, the observational catalog used to confront galactic dynamics models with data.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete falsification criteria that close the loop from the theoretical T0-T8 derivation to empirical tests of ILG in the gravity sector. It feeds the broader Recognition Science program by providing decidable predicates that would refute RS predictions if the SPARC median chi-squared exceeds the stated thresholds. The supplied doc-comment fixes the generous threshold at 5.0 for the chi-squared per dof test.

scope and limits

Does not contain the SPARC dataset or any fitting routines.
Does not compute chi-squared values from raw observations.
Does not claim that current data actually falsifies ILG.
Does not derive the numerical thresholds from the phi-ladder or RCL.

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