sparc_falsifier_cert
The SPARC falsifier certificate asserts that the ILG rotation curve model satisfies its zero-parameter falsification test against the SPARC sample when all parameters derive from phi. Galaxy dynamics researchers testing modified gravity would cite it to confirm the global-only protocol meets the decidable criterion. The proof is a term construction that directly assembles five supporting theorems into the certificate structure.
claimThe SPARC falsifier certificate holds when the number of per-galaxy free parameters equals zero, the parameters satisfy alpha locked to (1 - 1/phi)/2, upsilon locked to phi, and clag locked to phi to the power of -5, the falsification criterion is decidable for every real threshold, the global-only policy is satisfied, and the mean chi-squared per degree of freedom for ILG is strictly less than the corresponding MOND value.
background
The module formalizes a chi-squared falsification test for the ILG rotation curve prediction on the SPARC galaxy sample. The test requires zero per-galaxy free parameters, with all three RS parameters locked to values derived from phi: alpha equals (1 - 1/phi)/2, upsilon equals phi, and clag equals phi to the power of -5. The falsification criterion declares the model falsified if the median chi-squared per degree of freedom across the sample exceeds a chosen threshold; the decidability theorem shows this comparison is always resolved by a simple ordering against the generous threshold of 5.0.
proof idea
The proof is a term-mode construction of the SPARCFalsifierCert structure. It supplies zero_free_params for the zero_params field, parameters_from_phi for the params_from_phi field, falsification_decidable for the criterion_decidable field, global_only_policy for the global_only field, and ilg_better_mean_than_mond for the ilg_beats_mond_mean field.
why it matters in Recognition Science
This certificate completes the formal statement of the SPARC falsification protocol inside the Recognition Science gravity section. It encodes the requirement that ILG predictions use only globally locked phi-derived parameters (T5 J-uniqueness and T6 phi fixed point) and supplies a decidable test that can reject the model if median chi-squared per degree of freedom exceeds the threshold. The lower mean chi-squared relative to MOND is included to record that the global-only constraint improves outlier handling while still allowing falsification.
scope and limits
- Does not compute numerical chi-squared values from the SPARC data set.
- Does not fix the final threshold value used for rejection.
- Does not address systematic uncertainties beyond the generous threshold of 5.0.
- Does not claim the model passes the test, only that the certificate structure is inhabited.
formal statement (Lean)
186theorem sparc_falsifier_cert : SPARCFalsifierCert where
187 zero_params := zero_free_params
proof body
Term-mode proof.
188 params_from_phi := parameters_from_phi
189 criterion_decidable := falsification_decidable
190 global_only := global_only_policy
191 ilg_beats_mond_mean := ilg_better_mean_than_mond
192
193end SPARCFalsifier
194end Gravity
195end IndisputableMonolith