alpha_lock_at_scale

formal source

  25    The running coupling alpha_inv_running matches the geometric alphaLock
  26    at the lock-in scale lambda_rec = ell0.
  27    Note: This is the 'initial condition' for the RG flow from first principles. -/
  28theorem alpha_lock_at_scale :
  29    alpha_inv_running (effective_scale ell0) (effective_scale ell0) (1 / alpha_locked) = 1 / alpha_locked := by
  30  unfold alpha_inv_running
  31  rw [div_self (ne_of_gt (effective_scale_pos ell0_pos))]
  32  rw [Real.log_one, mul_zero, sub_zero]
  33
  34/-- **SCAFFOLD: Eight-Beat Plateau Dominance**
  35    Below the lock-in scale Q < Q_lock, the discrete eight-beat cycle
  36    prevents further running, maintaining the geometric value. -/
  37def is_locked_regime (Q : ℝ) : Prop := Q ≤ Q_lock
  38
  39/-- The physical coupling including the lock-in effect. -/
  40noncomputable def alpha_inv_phys (Q : ℝ) : ℝ :=
  41  if Q ≥ Q_lock then
  42    alpha_inv_running Q Q_lock (1 / alpha_locked)
  43  else
  44    1 / alpha_locked
  45
  46/-- **THEOREM: Physical Coupling Continuity**
  47    The physical coupling is continuous at the lock-in boundary.
  48    Both branches agree at Q = Q_lock (proved in `alpha_lock_at_scale`). -/
  49theorem alpha_inv_phys_continuous :
  50    ContinuousAt alpha_inv_phys Q_lock := by
  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