def
definition
beta0QCD
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.RGTransport on GitHub at line 102.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
99/-! ## Canonical one-loop beta/gamma kernels (Level-B groundwork) -/
100
101/-- One-loop QCD beta coefficient in the convention `beta0 = 11 - 2*nf/3`. -/
102def beta0QCD (nf : ℕ) : ℚ := (11 : ℚ) - (2 : ℚ) * nf / 3
103
104/-- Real-valued view of `beta0QCD`. -/
105def beta0QCDReal (nf : ℕ) : ℝ := (beta0QCD nf : ℝ)
106
107/-- One-loop QCD running for `alpha_s`:
108`d alpha_s / d ln mu = -(beta0/(2*pi)) * alpha_s^2`. -/
109noncomputable def betaQCD1L (nf : ℕ) (alphaS : ℝ) : ℝ :=
110 -((beta0QCDReal nf) / (2 * Real.pi)) * alphaS ^ 2
111
112/-- One-loop QED running with an effective charge-weight factor.
113This keeps the kernel explicit while allowing policy-level charge sums. -/
114noncomputable def betaQED1L (chargeWeight : ℝ) (alpha : ℝ) : ℝ :=
115 (chargeWeight / (3 * Real.pi)) * alpha ^ 2
116
117/-- Minimal one-loop mass anomalous-dimension scaffold for QCD.
118The exact scheme-dependent higher-loop expression is left to Level-B extensions. -/
119noncomputable def gammaMassQCD1L (alphaS : ℝ) : ℝ :=
120 (2 / Real.pi) * alphaS
121
122/-- Minimal one-loop mass anomalous-dimension scaffold for QED. -/
123noncomputable def gammaMassQED1L (chargeSq : ℝ) (alpha : ℝ) : ℝ :=
124 (3 * chargeSq / (4 * Real.pi)) * alpha
125
126theorem beta0QCD_nf0 : beta0QCD 0 = 11 := by
127 norm_num [beta0QCD]
128
129theorem beta0QCD_asymp_free (nf : ℕ) (hnf : nf ≤ 16) : 0 < beta0QCD nf := by
130 unfold beta0QCD
131 have hnfQ : (nf : ℚ) ≤ 16 := by
132 exact_mod_cast hnf