scale_at_two

formal source

  87  unfold phiLadderScale; norm_num
  88
  89/-- **THEOREM**: Scale at rung 2 is φ². -/
  90theorem scale_at_two : phiLadderScale 2 = phi^2 := by
  91  unfold phiLadderScale
  92  norm_cast
  93
  94/-- **THEOREM**: φ-ladder gives exponential hierarchy (φ^n > 1 for n > 0). -/
  95theorem phi_ladder_hierarchy (n : ℕ) (hn : n > 0) :
  96    phiLadderScale n > 1 := by
  97  unfold phiLadderScale
  98  rw [zpow_natCast]
  99  exact one_lt_pow₀ phi_gt_one' (Nat.pos_iff_ne_zero.mp hn)
 100
 101/-! ## Running Coupling Formula -/
 102
 103/-- The running coupling at φ-ladder rung n (1-loop approximation):
 104    α(n) = α₀ / (1 + b · n · ln φ) -/
 105noncomputable def runningCoupling (alpha0 b : ℝ) (n : ℤ) : ℝ :=
 106  alpha0 / (1 + b * n * log phi)
 107
 108/-- **THEOREM**: At rung 0, the coupling equals the reference value. -/
 109theorem running_at_zero (alpha0 b : ℝ) :
 110    runningCoupling alpha0 b 0 = alpha0 := by
 111  unfold runningCoupling
 112  simp
 113
 114/-- **THEOREM**: For positive b, coupling decreases with rung (asymptotic freedom). -/
 115theorem asymptotic_freedom_direction (alpha0 b : ℝ) (n : ℤ)
 116    (ha : alpha0 > 0) (hb : b > 0) (hn : n > 0) :
 117    runningCoupling alpha0 b n < alpha0 := by
 118  unfold runningCoupling
 119  have hlog : log phi > 0 := Real.log_pos (by linarith [phi_gt_onePointFive])
 120  have hbn_pos : b * n * log phi > 0 := by