alpha_inv_phys_continuous
plain-language theorem explainer
The theorem proves continuity of the physical inverse fine-structure constant at the lock-in scale Q_lock. Researchers matching renormalization-group flows to discrete geometric locking would cite it to confirm the coupling value is approached without jump. The argument builds an explicit piecewise function, verifies agreement on the frontier via alpha_lock_at_scale, proves separate continuity on each closed piece, and applies the continuous_if lemma to glue them at the boundary point.
Claim. Let $Q_lock$ be the lock-in scale and let $alpha_locked$ be the constant locked value. Define the function $alpha_inv_phys(q)$ to equal $alpha_inv_running(q, Q_lock, 1/alpha_locked)$ when $q >= Q_lock$ and to equal $1/alpha_locked$ otherwise. Then $alpha_inv_phys$ is continuous at $q = Q_lock$.
background
The module formalizes the transition from continuous RG flow to discrete geometric locking at the eight-beat plateau. Q_lock is defined as the effective scale of the fundamental length ell0, i.e., the recognition scale hbar/ell0. alpha_locked is the fixed value (1 - 1/phi)/2. The upstream lemma alpha_lock_at_scale shows that the running expression equals this locked value exactly at Q_lock. ell0_pos supplies the strict positivity of the base length needed to guarantee Q_lock > 0 and to control logarithms in the running expression.
proof idea
The proof first obtains Q_lock > 0 from effective_scale_pos applied to ell0_pos. It then shows that the running function equals the constant on the frontier of the half-line [Q_lock, infinity). Separate ContinuousOn statements are established: one for the running branch on the closed half-line (using continuity of log and arithmetic operations) and one for the constant branch on the complementary closure. These are combined by the continuous_if lemma to produce a globally continuous function, which is shown equal to alpha_inv_phys by function extensionality. Continuity at the single point Q_lock is then immediate.
why it matters
This result supplies the required continuity of the physical coupling at the lock-in boundary inside the CouplingLockIn module, ensuring the eight-tick octave plateau matches the running regime without discontinuity. It supports the claim that the locked coupling lies inside the observed alpha band. No downstream theorems are recorded, but the result is a prerequisite for any further scale-dependent analysis of couplings in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.