upsilon_locked
plain-language theorem explainer
Upsilon_locked assigns the stellar mass-to-light ratio exactly to phi in RS-native units for the ILG rotation-curve model. Galaxy dynamicists running zero-parameter SPARC falsification tests cite this lock to enforce the global-only policy. The declaration is a direct noncomputable assignment drawn from the phi constant.
Claim. $U_* = phi$ where $phi$ denotes the golden-ratio fixed point.
background
The SPARC Chi-Squared Falsifier module formalizes a median chi-squared test on ~175 galaxies that falsifies the ILG model when the median exceeds a chosen threshold under zero per-galaxy free parameters. Three RS parameters are locked from phi: alpha_t = (1 - 1/phi)/2, C_lag = phi^(-5), and Upsilon_star = phi. The module documentation states that all three parameters derive from phi and that the falsification protocol uses only catalog-level constants together with photometric baryonic profiles.
proof idea
One-line definition that directly assigns the imported phi constant to the mass-to-light ratio.
why it matters
The definition supplies the locked Upsilon value required by GlobalOnlyPolicy, parameters_from_phi, and SPARCFalsifierCert to certify that the ILG weight function depends on no per-galaxy parameters. It realizes the phi-ladder lock described in the module for the SPARC falsification criterion and connects to the T6 self-similar fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.