upsilon_locked
plain-language theorem explainer
Upsilon_locked defines the stellar mass-to-light ratio as equal to phi in Recognition Science units. Galaxy rotation-curve modelers testing the ILG prediction on SPARC data cite this definition to enforce the global-only policy with zero per-galaxy parameters. The declaration is a direct noncomputable assignment from the phi constant.
Claim. $Υ_* = ϕ ≈ 1.618$, where $ϕ$ is the self-similar fixed point of the Recognition Science forcing chain.
background
The SPARC Chi-Squared Falsifier module encodes the falsification test for the ILG rotation-curve model: compute median χ²/dof across the SPARC sample under zero free parameters; exceed the threshold and the model is falsified. All RS parameters are locked to phi-derived values, including alpha_t ≈ 0.191, C_lag ≈ 0.090, and Upsilon_star = phi ≈ 1.618. Upsilon_locked supplies the mass-to-light ratio component of this locking.
proof idea
Direct definition: upsilon_locked is assigned the constant phi. No lemmas or tactics are applied.
why it matters
This supplies the Upsilon_star value required by GlobalOnlyPolicy and SPARCFalsifierCert, which together certify the zero-parameter ILG prediction and the falsification criterion. It implements the RS parameter-locking step stated in the module documentation and feeds the parent theorem parameters_from_phi. The definition connects to the phi-ladder mass formula and the eight-tick octave via the forcing chain T5-T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.