alpha_inv_phys_continuous
plain-language theorem explainer
The theorem establishes that the physical inverse fine-structure constant is continuous at the lock-in scale. Researchers matching RG flow to geometric locking at the eight-beat plateau would cite it. The proof constructs the piecewise function explicitly, verifies branch agreement at the boundary via alpha_lock_at_scale, and invokes continuous_if after checking continuity of each piece on the respective closures.
Claim. The function giving the physical inverse fine-structure constant is continuous at the lock-in scale $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 fundamental recognition scale $Q_{lock} = hbar / ell_0$. The locked coupling value is $alpha_{locked} = (1 - 1/phi)/2$ (from Constants.ILG and Gravity.SPARCFalsifier). ell0_pos supplies the positivity of the base length unit ell0 in RS-native units.
proof idea
The tactic proof first obtains $0 < Q_{lock}$ from ell0_pos via effective_scale_pos. It shows the running branch equals the locked value on the frontier of the half-line using alpha_lock_at_scale. Continuity of the running piece on the closed half-line is proved by composing continuousAt for division, log, and scaling. The constant piece is trivially continuous. continuous_if is applied to the piecewise definition, which is then shown equal to alpha_inv_phys by funext and simp.
why it matters
This result supplies the continuity needed for the physical coupling in the lock-in mechanism of the module. It sits downstream of alpha_inv_phys and alpha_lock_at_scale, and upstream of any further RG matching. It touches the alpha band and the eight-tick octave (T7) in the forcing chain but leaves open whether higher derivatives exist at the boundary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.