su2_beta0

formal source

  65  rw [qcd_beta0_positive]; norm_num
  66
  67/-- **THEOREM**: SU(2) with 6 flavors has β₀ = 10/3 > 0. -/
  68theorem su2_beta0 : beta0_SUN 2 6 = 10/3 := by native_decide
  69
  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]