alpha_locked
plain-language theorem explainer
alpha_locked supplies the locked fine-structure constant (1 - 1/phi)/2 for the ILG rotation-curve model. SPARC falsification work in Gravity.SPARCFalsifier cites it to enforce zero per-galaxy parameters when computing median chi2/dof. The declaration is a direct noncomputable alias to the alphaLock constant defined in Constants.
Claim. $alpha_locked := (1 - phi^{-1})/2$
background
The SPARC Chi-Squared Falsifier module encodes the test that rejects the ILG model if the median chi-squared per degree of freedom across ~175 galaxies exceeds a chosen threshold when every parameter is fixed by phi. The three locked constants are alpha_t = (1 - 1/phi)/2, C_lag = phi^{-5}, and Upsilon_star = phi. Upstream, Constants defines the canonical value as alphaLock : ℝ := (1 - 1 / phi) / 2 with the accompanying identity that twice alphaLock clears the denominator in acceleration-parameterized exponents.
proof idea
One-line alias that unfolds directly to the alphaLock definition from Constants.
why it matters
The definition is referenced by GlobalOnlyPolicy, parameters_from_phi, and SPARCFalsifierCert, which together certify that the ILG prediction uses only catalog-level constants derived from phi and no kinematic fitting. It therefore implements the RS-native alpha inside the interval (137.030, 137.039) for the eight-tick octave and D = 3 setting. The same value appears in the downstream ILG lemmas that establish positivity and the strict upper bound less than one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.