alpha_inv_phys
plain-language theorem explainer
The definition supplies the scale-dependent inverse fine-structure constant that stays fixed at the locked value for Q below the lock-in threshold and switches to the running coupling above it. Physicists matching RG flows to geometric locking in Recognition Science would cite this when bridging low-energy constants to the eight-beat plateau. The construction is a direct piecewise definition that selects between the constant 1/alpha_locked and the output of alpha_inv_running.
Claim. $alpha^{-1}_{phys}(Q) := 1/alpha_{locked}$ if $Q < Q_{lock}$, and $alpha^{-1}_{phys}(Q) := alpha^{-1}_{running}(Q, Q_{lock}, 1/alpha_{locked})$ if $Q >= Q_{lock}$.
background
The module formalizes the transition from continuous RG flow to discrete geometric locking at the eight-beat plateau. Upstream, alpha_locked is defined as (1 - 1/phi)/2 in Constants.ILG, while the Physical structure from Bridge.DataCore encodes minimal assumptions c_pos, hbar_pos, G_pos on bridge anchors. The running function alpha_inv_running is supplied by the imported RunningCouplings module.
proof idea
Definition by cases on the predicate Q >= Q_lock, returning the constant 1/alpha_locked on the low side and the call to alpha_inv_running on the high side.
why it matters
This definition is the direct input to the continuity theorem alpha_inv_phys_continuous, which shows agreement of both branches at Q = Q_lock. It supplies the concrete realization of the lock-in step inside the eight-tick octave (T7) and the phi-ladder, closing the passage from continuous running to the discrete geometric regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.