alpha_inv_phys_continuous
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish continuity of alpha_inv_phys at any point other than Q_lock.
- Does not compute or bound the numerical value of the locked coupling.
- Does not address differentiability or higher regularity at the boundary.
- Does not derive the explicit form of the running coupling alpha_inv_running.
formal statement (Lean)
49theorem alpha_inv_phys_continuous :
50 ContinuousAt alpha_inv_phys Q_lock := by
proof body
Tactic-mode proof.
51 have hQlock_pos : 0 < Q_lock := by
52 simpa [Q_lock] using (effective_scale_pos ell0_pos)
53 have hp :
54 ∀ a ∈ frontier {x : ℝ | Q_lock ≤ x},
55 alpha_inv_running a Q_lock (1 / alpha_locked) = (1 / alpha_locked) := by
56 intro a ha
57 have haIci : a ∈ frontier (Set.Ici Q_lock) := by
58 simpa [Set.Ici] using ha
59 have ha' : a ∈ ({Q_lock} : Set ℝ) := (frontier_Ici_subset (a := Q_lock)) haIci
60 have hEq : a = Q_lock := by simpa using ha'
61 subst hEq
62 simpa [Q_lock] using alpha_lock_at_scale
63 have hf :
64 ContinuousOn
65 (fun q : ℝ => alpha_inv_running q Q_lock (1 / alpha_locked))
66 (closure {x : ℝ | Q_lock ≤ x}) := by
67 intro x hx
68 have hxClosure : x ∈ closure (Set.Ici Q_lock) := by
69 simpa [Set.Ici] using hx
70 have hxIci : x ∈ Set.Ici Q_lock := by
71 simpa [closure_Ici] using hxClosure
72 have hxge : Q_lock ≤ x := hxIci
73 have hxpos : 0 < x := lt_of_lt_of_le hQlock_pos hxge
74 have hdiv_ne : x / Q_lock ≠ 0 := by
75 exact div_ne_zero (ne_of_gt hxpos) (ne_of_gt hQlock_pos)
76 have hdiv_cont : ContinuousAt (fun q : ℝ => q / Q_lock) x := by
77 exact continuousAt_id.div_const Q_lock
78 have hlog_cont : ContinuousAt (fun q : ℝ => Real.log (q / Q_lock)) x := by
79 exact (ContinuousAt.comp (f := fun q : ℝ => q / Q_lock) (g := Real.log) (x := x)
80 (Real.continuousAt_log hdiv_ne) hdiv_cont)
81 have hscaled : ContinuousAt
82 (fun q : ℝ => (1 / (3 * Real.pi)) * Real.log (q / Q_lock)) x := by
83 exact hlog_cont.const_mul (1 / (3 * Real.pi))
84 have hmain : ContinuousAt
85 (fun q : ℝ => alpha_inv_running q Q_lock (1 / alpha_locked)) x := by
86 simpa [alpha_inv_running] using continuousAt_const.sub hscaled
87 exact hmain.continuousWithinAt
88 have hg :
89 ContinuousOn (fun _ : ℝ => (1 / alpha_locked : ℝ))
90 (closure {x : ℝ | ¬x ≥ Q_lock}) := by
91 simpa using (continuous_const.continuousOn :
92 ContinuousOn (fun _ : ℝ => (1 / alpha_locked : ℝ))
93 (closure {x : ℝ | ¬x ≥ Q_lock}))
94 have hcont :
95 Continuous (fun q : ℝ =>
96 if Q_lock ≤ q then alpha_inv_running q Q_lock (1 / alpha_locked) else (1 / alpha_locked)) := by
97 exact continuous_if hp hf hg
98 have hEqFun :
99 (fun q : ℝ =>
100 if Q_lock ≤ q then alpha_inv_running q Q_lock (1 / alpha_locked) else (1 / alpha_locked))
101 = alpha_inv_phys := by
102 funext q
103 simp [alpha_inv_phys, ge_iff_le]
104 have hcontAt :
105 ContinuousAt
106 (fun q : ℝ =>
107 if Q_lock ≤ q then alpha_inv_running q Q_lock (1 / alpha_locked) else (1 / alpha_locked))
108 Q_lock := hcont.continuousAt
109 rw [← hEqFun]
110 exact hcontAt
111
112end CouplingLockIn
113end Physics
114end IndisputableMonolith