parameters_from_phi
The declaration establishes that the three ILG parameters equal explicit functions of the golden ratio phi, enforcing zero free parameters per galaxy in the SPARC test. Rotation-curve analysts would cite it when applying the global-only policy to compare the ILG prediction against SPARC data. The proof is a one-line term wrapper that unfolds the locked definitions and closes by reflexivity.
claim$alpha_locked = (1 - phi^{-1})/2 land upsilon_locked = phi land clag_locked = phi^{-5}$
background
The SPARC Chi-Squared Falsifier module formalizes a test of the ILG rotation-curve model on the SPARC galaxy sample. All parameters must be locked to phi-derived values so that no per-galaxy freedom remains. The module documentation states: Use ZERO per-galaxy free parameters (all locked to phi). The locked constants are supplied by upstream definitions: alphaLock gives the fine-structure constant as (1 - 1/phi)/2, cLagLock gives the lag constant as phi^{-5}, and upsilon is taken directly as phi. These rest on phi-forcing results and ledger factorization from the foundation layer.
proof idea
The proof is a term-mode one-liner. It unfolds alpha_locked, upsilon_locked, clag_locked, alphaLock, and cLagLock, reducing each conjunct to an explicit phi expression. The exact tactic with the triple reflexivity then discharges the goal.
why it matters in Recognition Science
The result is invoked by global_only_policy to populate the alpha, upsilon, and clag fields and by sparc_falsifier_cert to certify the zero-parameter SPARC falsifier. It supplies the locked-parameter step required by the module's falsification protocol, aligning with Recognition Science's derivation of constants from phi (T5 J-uniqueness, T6 phi fixed point). It leaves open whether the resulting median chi-squared per degree of freedom exceeds the chosen thresholds.
scope and limits
- Does not evaluate chi-squared on any SPARC galaxy.
- Does not select or justify the falsification thresholds.
- Does not incorporate observational uncertainties or selection effects.
- Does not derive phi from the forcing chain.
Lean usage
alpha_from_phi := parameters_from_phi.1 upsilon_from_phi := parameters_from_phi.2.1 clag_from_phi := parameters_from_phi.2.2formal statement (Lean)
82theorem parameters_from_phi :
83 alpha_locked = (1 - 1/phi) / 2 ∧
84 upsilon_locked = phi ∧
85 clag_locked = phi ^ (-(5 : ℝ)) := by
proof body
Term-mode proof.
86 unfold alpha_locked upsilon_locked clag_locked alphaLock cLagLock
87 exact ⟨rfl, rfl, rfl⟩
88
89/-- The number of per-galaxy free parameters is exactly zero. -/