SPARCFalsifierCert
plain-language theorem explainer
SPARCFalsifierCert packages the five conditions needed to certify that the ILG rotation-curve model, run with zero per-galaxy parameters and constants locked to phi, meets the SPARC falsification protocol. Galaxy-dynamics researchers cite the structure when checking whether the median chi-squared per degree of freedom exceeds the generous threshold while still beating MOND. The definition simply assembles fields drawn from sibling definitions for the locked parameters, the decidable criterion, the global-only policy, and the mean-chi-squared (1
Claim. A certificate structure requiring: zero per-galaxy free parameters; the constants locked by $alpha = (1-1/phi)/2$, $Upsilon_* = phi$, $C_{lag} = phi^{-5}$; the decidable criterion that for every real $x$ either the model is falsified or passes according to the median chi-squared per degree of freedom; the global-only policy on the weight function; and the mean chi-squared of the ILG prediction strictly less than that of MOND.
background
The module formalizes the SPARC chi-squared falsifier for the ILG rotation-curve prediction. ILG_falsified holds precisely when the median chi-squared per degree of freedom exceeds the generous threshold; ILG_passes holds when the median lies at or below that threshold. GlobalOnlyPolicy requires that the ILG weight function depends only on catalog-level constants (alpha, C_lag, Upsilon) derived from phi and on the photometric baryonic profile, with no dependence on observed velocities or per-galaxy fits. Upstream, alpha_locked is defined as (1-1/phi)/2, clag_locked as phi^{-5}, and the same locking appears in the sibling GlobalOnlyPolicy structure.
proof idea
This is a structure definition with no proof body. It directly references the sibling definitions zero_free_params, parameters_from_phi, falsification_decidable, global_only_policy, and ilg_better_mean_than_mond to populate its five fields.
why it matters
The structure supplies the certificate object used by the downstream theorem sparc_falsifier_cert. It encodes the falsification protocol step in the Recognition Science gravity module, where all parameters are forced from phi (T5 J-uniqueness, T6 self-similar fixed point) and the model is required to satisfy the global-only policy with zero free parameters. It leaves open the numerical verification of the median chi-squared against actual SPARC data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.