parameters_from_phi
plain-language theorem explainer
The three ILG parameters equal explicit functions of phi, confirming zero free parameters in the SPARC falsifier. Modelers of galaxy rotation curves cite this to justify the global-only policy in chi-squared tests. The proof reduces to definition unfolding and reflexivity.
Claim. $alpha_locked = (1 - phi^{-1})/2 land upsilon_locked = phi land clag_locked = phi^{-5}$, where the left-hand sides are the ILG parameter definitions and the right-hand sides are the phi-locked constants.
background
The SPARC Chi-Squared Falsifier module tests the ILG rotation-curve model on the SPARC sample under a global-only policy. All three parameters must be locked to phi-derived values so that the number of per-galaxy free parameters is exactly zero. The module lists the locked values explicitly: alpha_t = (1 - 1/phi)/2, C_lag = phi^{-5}, Upsilon_star = phi.
proof idea
The term-mode proof unfolds alpha_locked, upsilon_locked, clag_locked, alphaLock and cLagLock, then closes with exact ⟨rfl, rfl, rfl⟩.
why it matters
The result is invoked by global_only_policy (which populates alpha_from_phi, upsilon_from_phi, clag_from_phi) and by sparc_falsifier_cert (which certifies the zero-params claim). It realizes the “RS Parameters (locked, from phi)” section of the module documentation and supplies the concrete phi expressions required by the falsification protocol. The construction is consistent with the phi-ladder and the self-similar fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.