 115    I_RS ∝ ln(p_max / m) = ln(ℏ / (l₀ × m × c))
 116
 117    This is finite! -/
 118noncomputable def regulatedIntegral (m Λ : ℝ) (hm : m > 0) (hΛ : Λ > m) : ℝ :=
 119  Real.log (Λ / m)
 120
 121/-- **THEOREM**: The RS-regulated integral is finite (for any finite cutoff). -/
 122theorem rs_integral_finite (m : ℝ) (hm : m > 0) (hpm : p_max > m) :
 123    ∃ (B : ℝ), regulatedIntegral m p_max hm hpm < B := by
 124  use Real.log (p_max / m) + 1
 125  unfold regulatedIntegral
 126  linarith
 127
 128/-! ## Running Couplings and the φ-Ladder -/
 129
 130/-- In QFT, coupling constants "run" with energy scale.
 131
 132    α(E) = α(E₀) / (1 - b × α(E₀) × ln(E/E₀))
 133
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.