IndisputableMonolith.Physics.QCDRGE.ThresholdMatching

   1import Mathlib
   2import IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
   3import IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension
   4
   5/-!
   6# Heavy Quark Threshold Matching (NLO)
   7
   8When running QCD couplings and quark masses across heavy-quark thresholds, the
   9number of active flavors changes. The matching condition at the quark threshold
  10mu_q (typically chosen as mu_q = m_q^MSbar) relates the (n+1)-flavor coupling
  11to the n-flavor coupling via finite matching coefficients:
  12
  13  alpha_s^(n)(mu_q) = alpha_s^(n+1)(mu_q) * (1 + sum_k c_k a^k)
  14
  15with c_1 = 0 at mu_q = m_q^MSbar (no leading log) and c_2 = 11/72 at NLO in
  16the standard MS-bar decoupling scheme.
  17
  18For quark masses at threshold:
  19
  20  m^(n)(mu_q) = m^(n+1)(mu_q) * (1 + sum_k d_k a^k)
  21
  22with d_1 = 0 at mu_q = m_q and d_2 = -89/432 in MS-bar.
  23
  24This module provides the structural matching infrastructure. It defines
  25the matching coefficients and proves the basic algebraic properties.
  26
  27## Status: 0 sorry, 0 axiom.
  28-/
  29
  30namespace IndisputableMonolith.Physics.QCDRGE.ThresholdMatching
  31
  32open IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
  33open IndisputableMonolith.Physics.QCDRGE.MassAnomalousDimension
  34
  35noncomputable section
  36
  37/-! ## Matching coefficients in MS-bar -/
  38
  39/-- NLO alpha_s matching coefficient at mu = m_q^MSbar.
  40    Standard result: c_2_alpha = 11/72. -/
  41def c_2_alpha : ℝ := 11 / 72
  42
  43/-- NLO mass matching coefficient at mu = m_q^MSbar.
  44    Standard result: d_2_mass = -89/432 (negative; mass slightly decreases). -/
  45def d_2_mass : ℝ := -89 / 432
  46
  47/-- Matching factor for alpha_s at threshold (NLO accuracy).
  48    Returns alpha_s^(n) given alpha_s^(n+1) at the threshold scale. -/
  49def alpha_match (alpha_above : ℝ) : ℝ :=
  50  alpha_above * (1 + c_2_alpha * (alpha_above / Real.pi) ^ 2)
  51
  52/-- Matching factor for the mass at threshold (NLO accuracy).
  53    Returns m^(n) given m^(n+1) at the threshold scale. -/
  54def mass_match (mass_above alpha_at_threshold : ℝ) : ℝ :=
  55  mass_above * (1 + d_2_mass * (alpha_at_threshold / Real.pi) ^ 2)
  56
  57/-! ## Positivity of matching factors
  58
  59For the small alpha values that occur at the heavy-quark thresholds
  60(alpha_s(m_b) ~ 0.22, alpha_s(m_c) ~ 0.38), the corrections are at the
  61percent level and never threaten positivity. We prove this conditionally
  62on the input being positive and the alpha being below 1 (perturbative). -/
  63
  64theorem alpha_match_pos (alpha_above : ℝ)
  65    (h_pos : 0 < alpha_above) (h_lt : alpha_above < 1) :
  66    0 < alpha_match alpha_above := by
  67  unfold alpha_match
  68  apply mul_pos h_pos
  69  have h_a_over_pi_pos : 0 < alpha_above / Real.pi :=
  70    div_pos h_pos Real.pi_pos
  71  have h_a_over_pi_sq_pos : 0 < (alpha_above / Real.pi) ^ 2 :=
  72    pow_pos h_a_over_pi_pos 2
  73  have h_c_pos : 0 < c_2_alpha := by unfold c_2_alpha; norm_num
  74  positivity
  75
  76theorem mass_match_pos (mass_above alpha_at_threshold : ℝ)
  77    (h_mass_pos : 0 < mass_above) (h_alpha_pos : 0 < alpha_at_threshold)
  78    (h_alpha_small : alpha_at_threshold < 1) :
  79    0 < mass_match mass_above alpha_at_threshold := by
  80  unfold mass_match
  81  apply mul_pos h_mass_pos
  82  -- d_2_mass = -89/432 ≈ -0.206. We bound (a/π)^2 < 1, so the correction is > -1.
  83  have h_d_gt : (-1 : ℝ) < d_2_mass := by unfold d_2_mass; norm_num
  84  have h_d_neg : d_2_mass < 0 := by unfold d_2_mass; norm_num
  85  have h_a_pos : 0 < alpha_at_threshold / Real.pi := div_pos h_alpha_pos Real.pi_pos
  86  have h_a_sq_pos : 0 < (alpha_at_threshold / Real.pi) ^ 2 := pow_pos h_a_pos 2
  87  -- Bound (a/π)^2 < 1: a < 1 and π > 1, so a/π < 1, so (a/π)^2 < 1.
  88  have h_pi_gt_one : (1 : ℝ) < Real.pi := by
  89    linarith [Real.pi_gt_three]
  90  have h_a_over_pi_lt_one : alpha_at_threshold / Real.pi < 1 := by
  91    rw [div_lt_one Real.pi_pos]; linarith
  92  have h_a_sq_lt_one : (alpha_at_threshold / Real.pi) ^ 2 < 1 := by
  93    have : (alpha_at_threshold / Real.pi) ^ 2 < 1 ^ 2 := by
  94      apply sq_lt_sq' <;> nlinarith [h_a_pos]
  95    simpa using this
  96  -- d_2_mass * x where x ∈ (0, 1), d_2_mass ∈ (-1, 0), so product ∈ (-1, 0).
  97  have h_prod_gt : -1 < d_2_mass * (alpha_at_threshold / Real.pi) ^ 2 := by
  98    nlinarith [h_d_gt, h_d_neg, h_a_sq_pos, h_a_sq_lt_one]
  99  linarith
 100
 101/-! ## Round-trip: matching plus its inverse is the identity to leading order -/
 102
 103/-- The matching at any threshold is a multiplicative perturbation; its inverse
 104    factor at NLO is `1 - c_2_alpha * (a/pi)^2 + O(a^4)`. We expose this as a
 105    structural definition rather than re-proving the perturbative inverse. -/
 106def alpha_unmatch (alpha_below : ℝ) : ℝ :=
 107  alpha_below * (1 - c_2_alpha * (alpha_below / Real.pi) ^ 2)
 108
 109/-! ## Master cert -/
 110
 111structure ThresholdMatchingCert where
 112  c_2_alpha_pos : 0 < c_2_alpha
 113  d_2_mass_neg : d_2_mass < 0
 114  alpha_match_pos_lemma : ∀ alpha_above : ℝ,
 115      0 < alpha_above → alpha_above < 1 → 0 < alpha_match alpha_above
 116  mass_match_pos_lemma : ∀ mass_above alpha_at_threshold : ℝ,
 117      0 < mass_above → 0 < alpha_at_threshold → alpha_at_threshold < 1 →
 118      0 < mass_match mass_above alpha_at_threshold
 119
 120theorem c_2_alpha_pos : 0 < c_2_alpha := by unfold c_2_alpha; norm_num
 121theorem d_2_mass_neg : d_2_mass < 0 := by unfold d_2_mass; norm_num
 122
 123theorem thresholdMatchingCert_holds : ThresholdMatchingCert :=
 124  { c_2_alpha_pos := c_2_alpha_pos
 125    d_2_mass_neg := d_2_mass_neg
 126    alpha_match_pos_lemma := alpha_match_pos
 127    mass_match_pos_lemma := mass_match_pos }
 128
 129end
 130
 131end IndisputableMonolith.Physics.QCDRGE.ThresholdMatching
 132