IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension

   1import Mathlib
   2import IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
   3
   4/-!
   5# Quark Mass Anomalous Dimension (MS-bar, two-loop)
   6
   7The MS-bar quark mass anomalous dimension governs the running of running
   8quark masses. To two loops, with C_F = 4/3 and N_f the number of active
   9flavors:
  10
  11  d log m / d log mu^2 = - gamma_m(alpha_s)
  12  gamma_m(a) = c_0 a + c_1 a^2 + O(a^3)
  13
  14with a = alpha_s / pi and:
  15  c_0 = 1                        (universal, sets normalization)
  16  c_1 = (101 N_c - 10 N_f) / 24 - 5/8 C_F   (canonical N_c=3 form: 67/12 - 5 N_f / 18)
  17
  18Solved to two loops, the running mass between scales mu and mu_0 is
  19
  20  m(mu) / m(mu_0) = (alpha_s(mu) / alpha_s(mu_0))^(c_0 / b0) * R(alpha_s(mu), alpha_s(mu_0))
  21
  22where R is the two-loop subleading correction.
  23
  24This module exposes the closed form, proves positivity, and connects to
  25the alpha_s running.
  26
  27## Status: 0 sorry, 0 axiom.
  28-/
  29
  30namespace IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension
  31
  32open IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
  33
  34noncomputable section
  35
  36/-- Leading mass anomalous dimension coefficient. -/
  37def c0 : ℝ := 1
  38
  39/-- Two-loop mass anomalous dimension coefficient (canonical N_c = 3 form). -/
  40def c1 (N_f : ℕ) : ℝ := 67 / 12 - 5 * (N_f : ℝ) / 18
  41
  42/-- The leading-log mass running ratio (one-loop accurate). -/
  43def mass_ratio_leading (alpha_mu alpha_mu_0 : ℝ) (N_f : ℕ) : ℝ :=
  44  Real.rpow (alpha_mu / alpha_mu_0) (c0 / b0 N_f)
  45
  46/-- The full two-loop mass running ratio. -/
  47def mass_ratio_two_loop (alpha_mu alpha_mu_0 : ℝ) (N_f : ℕ) : ℝ :=
  48  mass_ratio_leading alpha_mu alpha_mu_0 N_f *
  49  Real.exp ((c1 N_f / b0 N_f - c0 * b1 N_f / (b0 N_f) ^ 2) *
  50            (alpha_mu - alpha_mu_0) / (4 * Real.pi))
  51
  52/-! ## Positivity -/
  53
  54theorem b0_pos_at5 : 0 < b0 5 := b0_at_Nf5_pos
  55
  56theorem mass_ratio_leading_pos (alpha_mu alpha_mu_0 : ℝ) (N_f : ℕ)
  57    (h_alpha_pos : 0 < alpha_mu) (h_alpha_0_pos : 0 < alpha_mu_0) :
  58    0 < mass_ratio_leading alpha_mu alpha_mu_0 N_f := by
  59  unfold mass_ratio_leading
  60  exact Real.rpow_pos_of_pos (div_pos h_alpha_pos h_alpha_0_pos) _
  61
  62theorem mass_ratio_two_loop_pos (alpha_mu alpha_mu_0 : ℝ) (N_f : ℕ)
  63    (h_alpha_pos : 0 < alpha_mu) (h_alpha_0_pos : 0 < alpha_mu_0) :
  64    0 < mass_ratio_two_loop alpha_mu alpha_mu_0 N_f := by
  65  unfold mass_ratio_two_loop
  66  apply mul_pos
  67  · exact mass_ratio_leading_pos alpha_mu alpha_mu_0 N_f h_alpha_pos h_alpha_0_pos
  68  · exact Real.exp_pos _
  69
  70/-! ## Trivial reduction at the anchor -/
  71
  72theorem mass_ratio_leading_at_anchor (alpha_0 : ℝ) (N_f : ℕ)
  73    (h_alpha_pos : 0 < alpha_0) :
  74    mass_ratio_leading alpha_0 alpha_0 N_f = 1 := by
  75  unfold mass_ratio_leading
  76  rw [div_self (ne_of_gt h_alpha_pos)]
  77  exact Real.one_rpow _
  78
  79theorem mass_ratio_two_loop_at_anchor (alpha_0 : ℝ) (N_f : ℕ)
  80    (h_alpha_pos : 0 < alpha_0) :
  81    mass_ratio_two_loop alpha_0 alpha_0 N_f = 1 := by
  82  unfold mass_ratio_two_loop
  83  rw [mass_ratio_leading_at_anchor alpha_0 N_f h_alpha_pos]
  84  simp
  85
  86/-! ## The running quark mass
  87
  88`m_running mu m_0 mu_0 alpha_mu alpha_mu_0 N_f` returns the MS-bar quark mass
  89at scale `mu` given an anchor mass `m_0` at scale `mu_0` and the corresponding
  90alpha_s values. This is the engineering interface for the heavy-quark scorecards. -/
  91
  92def m_running (m_0 alpha_mu alpha_mu_0 : ℝ) (N_f : ℕ) : ℝ :=
  93  m_0 * mass_ratio_two_loop alpha_mu alpha_mu_0 N_f
  94
  95theorem m_running_pos (m_0 alpha_mu alpha_mu_0 : ℝ) (N_f : ℕ)
  96    (h_m0_pos : 0 < m_0) (h_alpha_pos : 0 < alpha_mu) (h_alpha_0_pos : 0 < alpha_mu_0) :
  97    0 < m_running m_0 alpha_mu alpha_mu_0 N_f := by
  98  unfold m_running
  99  exact mul_pos h_m0_pos
 100    (mass_ratio_two_loop_pos alpha_mu alpha_mu_0 N_f h_alpha_pos h_alpha_0_pos)
 101
 102theorem m_running_at_anchor (m_0 alpha_0 : ℝ) (N_f : ℕ)
 103    (h_alpha_pos : 0 < alpha_0) :
 104    m_running m_0 alpha_0 alpha_0 N_f = m_0 := by
 105  unfold m_running
 106  rw [mass_ratio_two_loop_at_anchor alpha_0 N_f h_alpha_pos]
 107  ring
 108
 109/-! ## Master cert -/
 110
 111structure MassAnomalousDimensionCert where
 112  c0_eq_one : c0 = 1
 113  c1_at5_pos : 0 < c1 5
 114  ratio_pos : ∀ (alpha_mu alpha_mu_0 : ℝ) (N_f : ℕ),
 115      0 < alpha_mu → 0 < alpha_mu_0 →
 116      0 < mass_ratio_two_loop alpha_mu alpha_mu_0 N_f
 117  ratio_anchor : ∀ (alpha_0 : ℝ) (N_f : ℕ),
 118      0 < alpha_0 → mass_ratio_two_loop alpha_0 alpha_0 N_f = 1
 119  running_pos : ∀ (m_0 alpha_mu alpha_mu_0 : ℝ) (N_f : ℕ),
 120      0 < m_0 → 0 < alpha_mu → 0 < alpha_mu_0 →
 121      0 < m_running m_0 alpha_mu alpha_mu_0 N_f
 122  running_anchor : ∀ (m_0 alpha_0 : ℝ) (N_f : ℕ),
 123      0 < alpha_0 → m_running m_0 alpha_0 alpha_0 N_f = m_0
 124
 125theorem c1_at5_pos : 0 < c1 5 := by unfold c1; norm_num
 126
 127theorem massAnomalousDimensionCert_holds : MassAnomalousDimensionCert :=
 128  { c0_eq_one := rfl
 129    c1_at5_pos := c1_at5_pos
 130    ratio_pos := mass_ratio_two_loop_pos
 131    ratio_anchor := mass_ratio_two_loop_at_anchor
 132    running_pos := m_running_pos
 133    running_anchor := m_running_at_anchor }
 134
 135end
 136
 137end IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension
 138