alpha_locked
plain-language theorem explainer
The definition supplies the locked fine-structure constant for use in RG flow and galaxy modeling. Workers on SPARC falsification or coupling lock-in cite it to fix the initial condition at the recognition scale. It is realized as a direct alias to the expression (1 - 1/phi)/2 from the constants module.
Claim. The locked fine-structure constant is given by $alpha_locked = (1 - phi^{-1})/2$.
background
The CouplingLockIn module formalizes the transition from continuous RG flow to discrete geometric locking at the eight-beat plateau. alpha_locked is the locked value of the fine-structure constant, introduced as the value that the running coupling matches at the lock-in scale lambda_rec = ell0. Upstream, alphaLock is defined in Constants as (1 - 1/phi)/2, and lambda_rec equals ell0 in RS-native units.
proof idea
This is a one-line wrapper that applies the definition of alphaLock from the Constants module.
why it matters
It supplies the alpha parameter to GlobalOnlyPolicy and parameters_from_phi in SPARCFalsifier, enforcing zero free parameters derived from phi. This fills the coupling lock-in step at the eight-tick octave (T7) of the forcing chain. The value anchors the discrete geometric initial condition for RG flow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.