alpha_inv_phys

formal source

  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
  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