runningCoupling

formal source

 134    In RS, this running follows the φ-ladder:
 135    - Energy scales are φ-spaced
 136    - Running between adjacent rungs is universal -/
 137noncomputable def runningCoupling (α0 b E E0 : ℝ) (hE : E > 0) (hE0 : E0 > 0) : ℝ :=
 138  α0 / (1 - b * α0 * Real.log (E / E0))
 139
 140/-- The φ-ladder gives discrete energy scales:
 141    E_n = E_0 × φ^n -/
 142noncomputable def phiLadderEnergy (E0 : ℝ) (n : ℤ) : ℝ :=
 143  E0 * phi^n
 144
 145/-- **THEOREM**: Adjacent φ-ladder rungs differ by factor φ. -/
 146theorem phi_ladder_ratio (E0 : ℝ) (hE0 : E0 ≠ 0) (n : ℤ) :
 147    phiLadderEnergy E0 (n + 1) / phiLadderEnergy E0 n = phi := by
 148  unfold phiLadderEnergy
 149  have hphi_ne : phi ≠ 0 := ne_of_gt Constants.phi_pos
 150  rw [mul_comm E0 (phi ^ (n + 1)), mul_comm E0 (phi ^ n)]
 151  rw [mul_div_mul_right _ _ hE0]
 152  rw [zpow_add_one₀ hphi_ne, mul_comm, mul_div_assoc]
 153  rw [div_self (zpow_ne_zero n hphi_ne), mul_one]
 154
 155/-! ## Implications for Renormalization -/
 156
 157/-- With a physical UV cutoff, renormalization becomes:
 158
 159    1. **Not just procedure**: The cutoff is physical, not artificial
 160    2. **Finite theory**: All loop integrals converge
 161    3. **Predictive**: Cutoff-dependent terms are measurable
 162    4. **Hierarchy**: Explains why large scale separations exist -/
 163def renormalizationImplications : List String := [
 164  "UV divergences are artifacts of continuum approximation",
 165  "The true theory is discrete and finite",
 166  "Renormalization is correct effective description",
 167  "Cutoff effects could be observable at high enough energies"