betaFunction

formal source

  51
  52/-- The beta function describes how a coupling changes with scale:
  53    β(g) = μ dg/dμ. For QED β > 0; for QCD β < 0 (asymptotic freedom). -/
  54def betaFunction : String := "β(g) = μ dg/dμ"
  55
  56/-- The 1-loop beta function coefficient for SU(N) with Nf flavors:
  57    β₀ = (11N - 2Nf) / 3 -/
  58def beta0_SUN (N Nf : ℕ) : ℚ := (11 * N - 2 * Nf) / 3
  59
  60/-- **THEOREM**: QCD (SU(3)) with 6 flavors has β₀ = 7 > 0. -/
  61theorem qcd_beta0_positive : beta0_SUN 3 6 = 7 := by native_decide
  62
  63/-- **THEOREM**: QCD is asymptotically free (positive β₀ means coupling decreases at high energy). -/
  64theorem qcd_asymptotic_free : beta0_SUN 3 6 > 0 := by
  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