`phiLadderScale`

definition

show as: view math explainer →

module: IndisputableMonolith.QFT.RunningCouplings
domain: QFT
line: 73 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.RunningCouplings on GitHub at line 73.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  70/-! ## φ-Ladder Connection -/
  71
  72/-- Energy scale at φ-ladder rung n, in units of reference scale E₀. -/
  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):

papers checked against this theorem

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