zero_free_params
Recognition Science's ILG rotation curve model for SPARC galaxies employs zero adjustable parameters per galaxy, with all constants locked to values derived from the golden ratio phi. Observers evaluating the model's predictive power against galaxy data would reference this equality to establish the parameter count. The proof reduces immediately to reflexivity on the explicit definition setting the count to zero.
claimThe number of per-galaxy free parameters in the ILG model is exactly zero: $N_ {rm free} = 0$.
background
The SPARC falsifier module tests the ILG rotation curve predictions under the Recognition Science framework with parameters fixed by phi. The sibling definition per_galaxy_free_parameters explicitly sets this count to zero, enforcing a global-only policy where alpha_t, Upsilon_star, and C_lag derive solely from phi without per-galaxy tuning. This setup follows the falsification protocol that computes median chi2/dof across the SPARC sample using the chi2 definition for summed squared residuals.
proof idea
The proof is a one-line wrapper applying reflexivity to the definition of per_galaxy_free_parameters, which is explicitly set to zero.
why it matters in Recognition Science
This anchors the global_only_policy theorem asserting all parameters come from phi and feeds into sparc_falsifier_cert that certifies the overall falsification criterion. It implements the zero free parameters requirement from the theory document line ~3304, ensuring the test of phi-locked predictions without tuning and closing the scaffolding for the SPARC benchmark.
scope and limits
- Does not evaluate the median chi2/dof for the SPARC sample.
- Does not establish the falsification threshold values of 3.0 or 5.0.
- Does not address systematic errors in the rotation curve data.
- Does not compare ILG predictions to MOND or other models.
Lean usage
theorem global_only_policy : GlobalOnlyPolicy where per_galaxy_params := zero_free_paramsformal statement (Lean)
92theorem zero_free_params : per_galaxy_free_parameters = 0 := rfl
proof body
Term-mode proof.
93
94/-! ## SPARC Benchmark Values
95
96The theory document (line ~3304) gives benchmark chi2 values.
97These are encoded as hypotheses (to be discharged by the Python script). -/
98
99/-- RS-predicted median chi2/dof across SPARC. -/