alpha_locked
plain-language theorem explainer
alpha_locked supplies the locked fine-structure constant α = (1 − 1/φ)/2 ≈ 0.191 for the zero-free-parameter ILG model inside the SPARC falsifier. Galaxy-modeling teams cite it when enforcing the global-only policy and testing the median-chi2 criterion. The declaration is a direct alias to the canonical alphaLock constant from Constants.
Claim. $α_{locked} := (1 - 1/φ)/2$
background
The SPARCFalsifier module formalizes the falsification protocol for the ILG rotation-curve model: compute predicted curves for the full SPARC sample using only catalog-level constants locked to φ, then reject the model if the median χ²/dof exceeds a chosen threshold. Three parameters are fixed from φ: alpha_t = (1 − 1/φ)/2, C_lag = φ^{-5}, Υ_star = φ. alpha_locked is the local identifier for the first of these inside the module. Upstream, Constants.alphaLock defines the same expression as the canonical locked fine-structure constant.
proof idea
one-line wrapper that applies alphaLock from Constants.
why it matters
The definition feeds GlobalOnlyPolicy, parameters_from_phi, and SPARCFalsifierCert, which together certify that the ILG weight function uses only phi-derived constants and zero per-galaxy parameters. It therefore implements the RS claim that the acceleration parameter is fixed by the self-similar fixed point φ without additional tuning. The same locked value appears in CouplingLockIn.alpha_inv_phys, closing the loop from the forcing chain to the empirical falsifier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.