m_c_PDG_GeV

formal source

  34/-! ## PDG charm mass -/
  35
  36/-- PDG 2024 m_c(m_c) MS-bar central, in GeV. -/
  37def m_c_PDG_GeV : ℝ := 1.27
  38
  39/-- PDG 2024 m_c(m_c) MS-bar uncertainty, in GeV. -/
  40def m_c_PDG_unc_GeV : ℝ := 0.02
  41
  42theorem m_c_PDG_pos : 0 < m_c_PDG_GeV := by unfold m_c_PDG_GeV; norm_num
  43
  44/-! ## RS prediction (structural) -/
  45
  46/-- RS rung for charm in the sector formula: r = 15 (up-type, generation 2). -/
  47def r_charm : ℕ := 15
  48
  49/-- A reference RS-anchored charm mass at the M_Z scale, used as the input
  50    `m_0` for two-loop mass running.
  51
  52    NOTE: this value is not derived in this module from first principles;
  53    the structural derivation is in `Masses.RSBridge.Anchor.massAtAnchor`
  54    via the gap-corrected formula. The numerical value here is the `massAtAnchor`
  55    output evaluated at the canonical RS yardstick. -/
  56def m_c_at_MZ_GeV : ℝ := 0.78  -- approximate MSbar charm at M_Z
  57
  58theorem m_c_at_MZ_pos : 0 < m_c_at_MZ_GeV := by unfold m_c_at_MZ_GeV; norm_num
  59
  60/-! ## Run from M_Z to m_c
  61
  62The RS prediction at the m_c scale is obtained by two-loop mass running from
  63M_Z down to m_c, using `mass_ratio_two_loop`. We expose the running engine
  64here; a final-row scorecard then compares to PDG. -/
  65
  66/-- The two-loop running prediction of m_c at its own scale, given input
  67    alpha_s values at M_Z and at m_c. -/