sparc_falsifier_cert
plain-language theorem explainer
The SPARC falsifier certificate asserts that the ILG rotation-curve model satisfies the zero per-galaxy free-parameter requirement together with the global-only policy and the decidable falsification criterion. Galaxy dynamicists would cite it when certifying that Recognition Science predictions remain testable against the SPARC sample. The proof is a term-mode structure constructor that assembles the certificate directly from five upstream lemmas on parameter locking and decidability.
Claim. There exists a certificate $C$ such that the number of per-galaxy free parameters equals zero, the parameters satisfy $alpha = (1 - phi^{-1})/2$, $Upsilon_* = phi$, $C_{lag} = phi^{-5}$, the predicate (median chi-squared per degree of freedom exceeds threshold) is decidable for every real threshold, the policy enforces globally locked parameters only, and the mean chi-squared of ILG is strictly lower than that of MOND.
background
The module formalizes a falsification test for the ILG rotation-curve model on the SPARC galaxy sample. Core definitions are per_galaxy_free_parameters (count of adjustable parameters per galaxy), alpha_locked/upsilon_locked/clag_locked (the three RS parameters fixed by phi), ILG_falsified x (median chi2/dof > threshold), ILG_passes x (the complementary case), and GlobalOnlyPolicy (all parameters derived from phi with no per-galaxy tuning). The module documentation states the protocol: compute ILG curves for ~175 galaxies, lock every parameter to phi expressions, form the median chi2/dof, and falsify if the median exceeds the chosen threshold (generous 5.0 or tight 3.0).
proof idea
The proof is a term-mode structure constructor for SPARCFalsifierCert. It supplies the five required fields by direct reference to the lemmas zero_free_params, parameters_from_phi, falsification_decidable, global_only_policy, and ilg_better_mean_than_mond.
why it matters
This declaration supplies the top-level certificate that the ILG model is formally falsifiable under the Recognition Science parameter lock. It completes the falsification protocol described in the module documentation, which implements the claim that median chi2/dof is approximately 2.75. No downstream uses are recorded, indicating it serves as the interface to external numerical checks. It touches the open question of whether the actual SPARC data will exceed the generous threshold of 5.0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.