IndisputableMonolith.Physics.CouplingLockIn

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Physics.RunningCouplings
   4
   5/-!
   6# Coupling Lock-in Mechanism
   7This module formalizes the transition from continuous RG flow to discrete
   8geometric locking at the eight-beat plateau.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Physics
  13namespace CouplingLockIn
  14
  15open Constants
  16
  17/-- The lock-in scale is the fundamental recognition scale Q_lock = hbar / ell0. -/
  18noncomputable def Q_lock : ℝ := effective_scale ell0
  19
  20/-- The locked value of the fine-structure constant.
  21    By Phase 2, this is alphaLock = (1 - 1/phi) / 2. -/
  22noncomputable def alpha_locked : ℝ := alphaLock
  23
  24/-- **THEOREM: Lock-in Condition**
  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
  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
 115