Q_lock
plain-language theorem explainer
Q_lock defines the recognition scale at which the fine-structure constant locks to its geometric value alphaLock. Physicists modeling the transition from RG flow to discrete locking cite this as the boundary between continuous running and the eight-beat plateau. The definition is a direct abbreviation of the effective_scale function applied to the base length ell0.
Claim. The lock-in scale is defined by $Q_{lock} :=$ effective_scale$($ell$_0)$, where ell$_0$ is the fundamental length unit and effective_scale yields the recognition scale equivalent to hbar / ell$_0$.
background
The module formalizes the transition from continuous renormalization-group flow to discrete geometric locking at the eight-beat plateau. ell0 is the fundamental length unit, defined as ell0 := 1 in RS-native units or equivalently c * tau0 with tau0^2 = hbar G / (pi c^5). alphaLock is the canonical locked fine-structure constant (1 - 1/phi)/2. Upstream results supply the phi-tier structure of nuclear densities and the ledger factorization of the J-cost.
proof idea
One-line definition that applies the effective_scale function to ell0.
why it matters
This supplies the boundary scale used by alpha_inv_phys to switch between running and locked regimes. It feeds the theorem alpha_lock_at_scale establishing that alpha_inv_running matches alphaLock at this scale, and the continuity result alpha_inv_phys_continuous. It realizes the eight-beat plateau dominance (T7) that closes the forcing chain from continuous flow to discrete locking.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.