zero_free_params
plain-language theorem explainer
The theorem asserts that the ILG rotation-curve model for the SPARC sample uses exactly zero per-galaxy free parameters. Analysts constructing falsification tests for Recognition Science gravity predictions cite this result to confirm that alpha, upsilon_star and C_lag remain locked to their phi-derived values. The proof is a direct reflexivity step on the definition of per_galaxy_free_parameters.
Claim. The number of per-galaxy free parameters required by the ILG model is zero: $N_ {rm per-galaxy}=0$.
background
The SPARC falsifier module encodes the protocol that computes median chi-squared per degree of freedom for ILG-predicted rotation curves across the SPARC sample. All parameters must be taken from the global phi ladder (alpha_t = (1-1/phi)/2, C_lag = phi^{-5}, Upsilon_star = phi) with no galaxy-specific adjustments permitted. The sibling definition per_galaxy_free_parameters : ℕ := 0 directly encodes this zero-parameter constraint.
proof idea
The proof is the one-line term rfl that applies reflexivity to the definition per_galaxy_free_parameters := 0.
why it matters
zero_free_params supplies the zero_params field of sparc_falsifier_cert and the per_galaxy_params field of global_only_policy. It implements the explicit requirement in the module documentation that the falsification test be performed with zero per-galaxy free parameters. The result therefore connects the phi-ladder constants (T5 J-uniqueness, T6 phi fixed point) to a concrete observational test on galaxy data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.