alpha_lock_at_scale
plain-language theorem explainer
The theorem establishes that the running inverse coupling equals its locked geometric value at the fundamental scale ell0. Researchers modeling renormalization group flows in Recognition Science cite this as the initial condition for coupling evolution from first principles. The term-mode proof unfolds the running definition and reduces the expression by canceling the logarithmic deviation using positivity of the scale.
Claim. At the lock-in scale corresponding to the fundamental length ell0, the running inverse fine-structure constant satisfies alpha^{-1}_running(Q_0, Q_0, 1/alpha_locked) = 1/alpha_locked, where Q_0 denotes the effective scale at ell0 and alpha_locked = (1 - phi^{-1})/2.
background
The Coupling Lock-in module formalizes the transition from continuous renormalization group flow to discrete geometric locking at the eight-beat plateau. Key definitions include ell0 as the fundamental length unit in RS-native units (with ell0_pos establishing positivity) and alpha_locked defined as (1 - 1/phi)/2. Upstream results derive ell0 from the light-cone identity ell0 = c * tau0 where tau0^2 = hbar G / (pi c^5), and introduce the scale function as phi raised to integer powers.
proof idea
The term proof first unfolds the definition of the running inverse coupling. It then rewrites using division by the positive effective scale at ell0, substitutes the logarithm of one to obtain zero, and cancels the resulting zero terms from multiplication and subtraction.
why it matters
This supplies the initial condition for the RG flow and is invoked to define the physical inverse coupling alpha_inv_phys together with the continuity theorem alpha_inv_phys_continuous at the lock-in boundary. It realizes the lock-in at the eight-tick octave in the forcing chain, with the locked value arising from the phi self-similar fixed point via the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.