`b0_qcd`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.RunningCouplings
domain: Physics
line: 53 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.RunningCouplings on GitHub at line 53.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  50/-- **ONE-LOOP QCD β-FUNCTION COEFFICIENT**:
  51    b₀ = 11 - 2n_f/3 where n_f is the number of active quark flavors.
  52    Asymptotic freedom requires b₀ > 0, i.e., n_f < 16.5. -/
  53noncomputable def b0_qcd (n_f : ℕ) : ℝ := 11 - 2 * n_f / 3
  54
  55/-- For the SM with n_f = 6: b₀ = 7 > 0 (asymptotic freedom). -/
  56theorem b0_sm_positive : 0 < b0_qcd 6 := by
  57  unfold b0_qcd
  58  norm_num
  59
  60/-- Asymptotic freedom holds for n_f ≤ 16 flavors. -/
  61theorem asymptotic_freedom_criterion (n_f : ℕ) (h : n_f ≤ 16) :
  62    0 < b0_qcd n_f := by
  63  unfold b0_qcd
  64  have : (n_f : ℝ) ≤ 16 := by exact_mod_cast h
  65  linarith
  66
  67/-- For n_f ≥ 17 flavors, QCD loses asymptotic freedom. -/
  68theorem no_asymptotic_freedom_17 : b0_qcd 17 ≤ 0 := by
  69  unfold b0_qcd
  70  norm_num
  71
  72/-- **CRITICAL FLAVOR NUMBER**: n_f < 16.5 for asymptotic freedom. -/
  73theorem critical_flavor_number : b0_qcd 16 > 0 ∧ b0_qcd 17 ≤ 0 := by
  74  constructor
  75  · unfold b0_qcd; norm_num
  76  · unfold b0_qcd; norm_num
  77
  78/-! ## Running α_s -/
  79
  80/-- **ONE-LOOP RUNNING α_s**:
  81    α_s(μ) = α_s(μ*) / (1 + b₀/(2π) × α_s(μ*) × ln(μ/μ*)) -/
  82noncomputable def alpha_s_running (α_s_anchor b₀ μ μ_star : ℝ) : ℝ :=
  83  α_s_anchor / (1 + b₀ / (2 * Real.pi) * α_s_anchor * Real.log (μ / μ_star))

papers checked against this theorem

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