per_galaxy_free_parameters
plain-language theorem explainer
The definition assigns zero to the count of per-galaxy free parameters in the ILG rotation curve model. Researchers auditing Recognition Science gravity predictions against SPARC observations cite this to lock all constants to phi-derived values with no per-object tuning. The declaration is a constant definition in the natural numbers.
Claim. The number of free parameters per galaxy in the ILG model equals $0$.
background
The SPARC falsifier module encodes the test for the ILG model, which predicts galactic rotation curves from baryonic mass distributions using only phi-locked constants. These constants are alpha_t = (1 - 1/phi)/2, C_lag = phi^{-5}, and Upsilon_star = phi. The protocol computes median chi-squared per degree of freedom across the sample and falsifies the model if it exceeds a chosen threshold. This definition ensures the model uses no adjustable parameters per galaxy, enforcing the global-only policy.
proof idea
The definition directly sets the value to the natural number zero. It requires no lemmas or tactics beyond the constant assignment itself. The zero_free_params theorem then recovers the equality by reflexivity.
why it matters
This definition supplies the zero-parameter constraint required by the GlobalOnlyPolicy and SPARCFalsifierCert structures. It implements the falsification protocol outlined in the module documentation, which tests the ILG prediction from the theory document against SPARC data. The zero count aligns with the framework's emphasis on phi as the sole source of constants, closing the loop from the forcing chain to observable falsifiability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.