IndisputableMonolith.Physics.QCDRGE.PoleToMSbar

   1import Mathlib
   2import IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
   3
   4/-!
   5# Pole Mass to MS-bar Mass Conversion (Two-Loop)
   6
   7The PDG top-quark mass is reported as the pole mass; charm and bottom are
   8reported as MS-bar at their own scale. To compare RS predictions across all
   9quarks we need the pole-to-MS-bar conversion.
  10
  11The relation, to two-loop accuracy in MS-bar with C_F = 4/3:
  12
  13  m_pole = m_MS(m_MS) * (1 + (4/3) (alpha_s/pi) + K_2 (alpha_s/pi)^2 + O(alpha_s^3))
  14
  15where K_2 ≈ 11.1 - 1.04 N_l (with N_l the number of light flavors) is the
  16two-loop coefficient. For top: N_l = 5, K_2 ≈ 11.1 - 5.2 = 5.9.
  17
  18This module exposes the closed form, proves positivity, and provides the
  19inverse direction.
  20
  21## Status: 0 sorry, 0 axiom.
  22-/
  23
  24namespace IndisputableMonolith.Physics.QCDRGE.PoleToMSbar
  25
  26open IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
  27
  28noncomputable section
  29
  30/-- One-loop pole-to-MS-bar coefficient: 4/3 (universal, from C_F). -/
  31def K_1 : ℝ := 4 / 3
  32
  33/-- Two-loop pole-to-MS-bar coefficient (canonical N_l = 5 for top quark). -/
  34def K_2 (N_l : ℕ) : ℝ := 11.1 - 1.04 * (N_l : ℝ)
  35
  36/-- The two-loop pole-to-MS-bar conversion factor.
  37
  38    `pole_factor alpha_s N_l = 1 + (4/3)(a/π) + K_2 (a/π)^2`
  39-/
  40def pole_factor (alpha_s : ℝ) (N_l : ℕ) : ℝ :=
  41  1 + K_1 * (alpha_s / Real.pi) + K_2 N_l * (alpha_s / Real.pi) ^ 2
  42
  43/-- Convert MS-bar mass at its own scale to pole mass. -/
  44def m_pole_from_MS (m_MS alpha_s : ℝ) (N_l : ℕ) : ℝ :=
  45  m_MS * pole_factor alpha_s N_l
  46
  47/-! ## Positivity (in the perturbative regime) -/
  48
  49theorem pole_factor_pos_top (alpha_s : ℝ)
  50    (h_alpha_pos : 0 < alpha_s) (h_alpha_lt : alpha_s < 0.5) :
  51    0 < pole_factor alpha_s 5 := by
  52  unfold pole_factor K_1 K_2
  53  have h_a_pos : 0 < alpha_s / Real.pi := div_pos h_alpha_pos Real.pi_pos
  54  have h_a_sq_pos : 0 < (alpha_s / Real.pi) ^ 2 := pow_pos h_a_pos 2
  55  have h_K2_at5_pos : 0 < (11.1 - 1.04 * (5 : ℝ)) := by norm_num
  56  -- 1 + positive + positive > 0 trivially
  57  have h1 : 0 < 1 + (4 / 3) * (alpha_s / Real.pi) := by
  58    have : 0 < (4 / 3) * (alpha_s / Real.pi) := mul_pos (by norm_num) h_a_pos
  59    linarith
  60  nlinarith [h_K2_at5_pos, h_a_sq_pos]
  61
  62theorem m_pole_from_MS_pos_top (m_MS alpha_s : ℝ)
  63    (h_m_MS_pos : 0 < m_MS) (h_alpha_pos : 0 < alpha_s) (h_alpha_lt : alpha_s < 0.5) :
  64    0 < m_pole_from_MS m_MS alpha_s 5 := by
  65  unfold m_pole_from_MS
  66  exact mul_pos h_m_MS_pos (pole_factor_pos_top alpha_s h_alpha_pos h_alpha_lt)
  67
  68/-! ## Inverse direction (MS-bar from pole)
  69
  70To NLO this is just `1 - K_1 (a/π)`; to two-loop one solves the perturbative
  71inverse explicitly. We expose the closed form. -/
  72
  73def inv_pole_factor (alpha_s : ℝ) (N_l : ℕ) : ℝ :=
  74  1 - K_1 * (alpha_s / Real.pi) +
  75  (K_1 ^ 2 - K_2 N_l) * (alpha_s / Real.pi) ^ 2
  76
  77def m_MS_from_pole (m_pole alpha_s : ℝ) (N_l : ℕ) : ℝ :=
  78  m_pole * inv_pole_factor alpha_s N_l
  79
  80/-- The inverse expression is positive for small enough alpha_s. The product
  81    `pole_factor * inv_pole_factor` agrees with 1 to two-loop accuracy
  82    (i.e., differs only by terms of order `alpha_s^3` or higher), but we do
  83    not state that algebraic identity explicitly here; it is straightforward
  84    algebra and not used in the downstream scorecards. -/
  85theorem inv_pole_factor_at_zero (N_l : ℕ) :
  86    inv_pole_factor 0 N_l = 1 := by
  87  unfold inv_pole_factor
  88  simp
  89
  90/-! ## Master cert -/
  91
  92structure PoleToMSbarCert where
  93  K_1_eq : K_1 = 4 / 3
  94  K_2_at5_pos : 0 < K_2 5
  95  pole_factor_pos_lemma : ∀ alpha_s : ℝ,
  96      0 < alpha_s → alpha_s < 0.5 → 0 < pole_factor alpha_s 5
  97  m_pole_pos_lemma : ∀ m_MS alpha_s : ℝ,
  98      0 < m_MS → 0 < alpha_s → alpha_s < 0.5 →
  99      0 < m_pole_from_MS m_MS alpha_s 5
 100
 101theorem K_2_at5_pos : 0 < K_2 5 := by unfold K_2; norm_num
 102
 103theorem poleToMSbarCert_holds : PoleToMSbarCert :=
 104  { K_1_eq := rfl
 105    K_2_at5_pos := K_2_at5_pos
 106    pole_factor_pos_lemma := pole_factor_pos_top
 107    m_pole_pos_lemma := m_pole_from_MS_pos_top }
 108
 109end
 110
 111end IndisputableMonolith.Physics.QCDRGE.PoleToMSbar
 112