alpha_inv_phys_continuous
plain-language theorem explainer
The inverse fine-structure constant in the physical regime is continuous at the lock-in scale Q_lock. Researchers matching continuous renormalization-group flow to discrete geometric locking at the eight-beat plateau would cite this result. The proof first verifies that the running and locked branches agree exactly at Q_lock using alpha_lock_at_scale, establishes continuity of each piece on the appropriate closed sets, and concludes via the continuous_if lemma that the piecewise definition is continuous at the boundary point.
Claim. The map $qmapsto alpha^{-1}_{rm phys}(q)$ is continuous at $q=Q_{rm lock}$, where $Q_{rm lock}$ is the fundamental recognition scale $hbar/ell_0$ and $alpha^{-1}_{rm phys}$ equals the running inverse coupling for $qge Q_{rm lock}$ and equals the locked value $1/alpha_{rm locked}$ otherwise.
background
In the Coupling Lock-in module the transition from continuous RG flow to discrete geometric locking is formalized at the eight-beat plateau. The lock-in scale is defined as $Q_{rm lock}=hbar/ell_0$, with $ell_0$ the fundamental length unit whose positivity follows from ell0_pos. The locked inverse coupling is the constant $1/alpha_{rm locked}$ with $alpha_{rm locked}=(1-1/phi)/2$. The running coupling alpha_inv_running appears in the definition of alpha_inv_phys, which switches from the running expression to the constant value below Q_lock.
proof idea
The tactic proof begins by establishing positivity of Q_lock via effective_scale_pos applied to ell0_pos. It then shows that on the frontier of the set {x | Q_lock ≤ x} the running expression reduces to the constant value by substituting a = Q_lock and invoking alpha_lock_at_scale. Continuity of the running piece on the closure of that set is proved by direct computation of the continuousAt properties of the logarithm and scaling factors inside alpha_inv_running. The constant piece is trivially continuous on the complementary closed set. The continuous_if lemma is applied to obtain continuity of the piecewise function, which is then shown to coincide with alpha_inv_phys by extensionality, yielding the desired ContinuousAt at Q_lock.
why it matters
This result closes the continuity requirement for the physical coupling at the lock-in boundary, ensuring that the transition from running to locked regime introduces no discontinuity in the inverse fine-structure constant. It supports the broader Coupling Lock-in Mechanism that formalizes the eight-beat plateau where continuous RG flow meets discrete geometry. The parent construction alpha_inv_phys is the object whose continuity is asserted here; downstream applications in running couplings and gravity models rely on this smoothness for consistent matching across scales. No open scaffolding remains in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.