global_only_policy
plain-language theorem explainer
The global-only policy theorem establishes that the ILG weight function depends solely on catalog-level constants derived from phi together with the photometric baryonic profile. Galaxy dynamics researchers testing the Recognition Science rotation-curve prediction against SPARC data would cite this result to lock the model to zero per-galaxy parameters. The proof is a direct term-mode construction that populates the four fields of the GlobalOnlyPolicy structure from the parameters_from_phi theorem and the zero_free_params lemma.
Claim. The ILG model satisfies the global-only policy when its parameters are locked to the Recognition Science values: $alpha_locked = (1 - 1/phi)/2$, $upsilon_locked = phi$, $clag_locked = phi^{-5}$, and the number of per-galaxy free parameters equals zero.
background
The GlobalOnlyPolicy structure requires that the ILG weight function w(r) depends only on catalog-level constants (alpha, C_lag, Upsilon) and the photometric baryonic profile, excluding observed velocities and per-galaxy fits. The module documentation states that the SPARC falsifier computes chi-squared per degree of freedom across the sample using parameters fixed by phi, with thresholds of 5.0 (generous) and 3.0 (tight) for falsification testing.
proof idea
The proof is a term-mode construction of the GlobalOnlyPolicy structure. It assigns alpha_from_phi to the first projection of parameters_from_phi, upsilon_from_phi to the second projection, clag_from_phi to the third projection, and per_galaxy_params to the zero_free_params theorem.
why it matters
This theorem supplies the global_only field required by the downstream sparc_falsifier_cert theorem that certifies the overall SPARC falsification protocol. It closes the parameter-locking step, ensuring the ILG prediction uses the RS-native values alpha = (1-1/phi)/2, Upsilon = phi, and C_lag = phi^{-5} with zero free parameters per galaxy. The result supports the claim that median chi2/dof above threshold falsifies the model under the global-only regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.