Q_lock
Q_lock defines the lock-in scale as effective_scale applied to ell0. It marks the fundamental recognition scale where RG flow halts and couplings lock to the geometric value. Researchers modeling renormalization group flows in Recognition Science cite it as the boundary for the eight-beat plateau. The definition is a direct one-line abbreviation pulling ell0 from the constants module.
claimThe lock-in scale is defined by $Q_{lock} = $ effective scale at the fundamental length unit $ell_0$, where $ell_0$ is the base voxel length in RS-native units.
background
The Coupling Lock-in Mechanism module formalizes the transition from continuous RG flow to discrete geometric locking at the eight-beat plateau. ell0 is the fundamental length unit in RS-native units (voxel). alphaLock is the canonical locked fine-structure constant: α_lock = (1 − 1/φ)/2. Upstream, the of structure in NucleosynthesisTiers organizes nuclear densities and photon fluxes on phi-tiers, with nuclear density ρ_nuc ~ φ^{n_nuclear} × ρ_Planck. The LedgerFactorization structure handles the J-cost and calibration of J.
proof idea
This is a one-line wrapper that applies the effective_scale function to ell0.
why it matters in Recognition Science
Q_lock supplies the boundary scale used by alpha_inv_phys to switch between running and locked regimes for the physical coupling, and by alpha_lock_at_scale to establish that the running coupling matches the geometric alphaLock at this point. It fills the coupling lock-in step in the Recognition Science framework, anchoring the eight-tick octave (T7) where the discrete cycle prevents further running. It touches the open question of continuity at the boundary, as addressed in alpha_inv_phys_continuous.
scope and limits
- Does not derive ell0 from the unified forcing chain.
- Does not prove the locking condition or continuity at the boundary.
- Does not compute the numerical value of Q_lock in SI units.
- Does not address the alpha inverse band or Berry creation threshold.
Lean usage
alpha_inv_phys Q_lockformal statement (Lean)
18noncomputable def Q_lock : ℝ := effective_scale ell0
proof body
Definition body.
19
20/-- The locked value of the fine-structure constant.
21 By Phase 2, this is alphaLock = (1 - 1/phi) / 2. -/