zero_free_params
plain-language theorem explainer
The zero_free_params theorem records that the ILG rotation-curve model employs exactly zero per-galaxy free parameters. Researchers comparing Recognition Science predictions to SPARC data cite it to enforce the global-only policy before computing median chi-squared. The proof is a single reflexivity step on the definition of per_galaxy_free_parameters.
Claim. The number of per-galaxy free parameters is zero: $N=0$.
background
The SPARC falsifier module tests the ILG model with every parameter locked to phi-derived constants (alpha_t, C_lag, Upsilon_star). The sibling definition per_galaxy_free_parameters sets the count of adjustable per-galaxy parameters to zero by construction, matching the falsification protocol that requires zero free parameters when median chi2/dof is evaluated across the sample. The upstream chi2 definition supplies the sum-of-squares metric used downstream, while the as structure from ContinuumBridge supplies the Laplacian identification underlying the gravity ledger.
proof idea
Term-mode proof consisting of a single reflexivity (rfl) on the definition per_galaxy_free_parameters := 0.
why it matters
Supplies the zero_params field required by sparc_falsifier_cert and the per_galaxy_params field of global_only_policy. It encodes the zero-per-galaxy requirement stated in the module documentation for the falsification test against SPARC. The result closes the global-only policy step that precedes any median-chi2 comparison and aligns with the phi-ladder locking of all constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.