phi_ne_zero'

formal source

  73noncomputable def phiLadderScale (n : ℤ) : ℝ := phi ^ n
  74
  75/-- φ is nonzero. -/
  76lemma phi_ne_zero' : phi ≠ 0 := ne_of_gt Constants.phi_pos
  77
  78/-- φ > 1. -/
  79lemma phi_gt_one' : phi > 1 := by linarith [phi_gt_onePointFive]
  80
  81/-- **THEOREM**: Scale at rung 0 is 1. -/
  82theorem scale_at_zero : phiLadderScale 0 = 1 := by
  83  unfold phiLadderScale; norm_num
  84
  85/-- **THEOREM**: Scale at rung 1 is φ. -/
  86theorem scale_at_one : phiLadderScale 1 = phi := by
  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)