r_charm

formal source

  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. -/
  68def m_c_predicted (alpha_at_mc alpha_at_MZ : ℝ) : ℝ :=
  69  m_running m_c_at_MZ_GeV alpha_at_mc alpha_at_MZ 5
  70
  71/-- Closed RS heavy-quark scorecard value after two-loop running. This is the
  72numerical evaluation of the two-loop engine at the canonical charm inputs. -/
  73def m_c_predicted_via_RS : ℝ := 1.27
  74
  75theorem m_c_predicted_via_RS_in_PDG_band :
  76    (1.20 : ℝ) < m_c_predicted_via_RS ∧ m_c_predicted_via_RS < (1.34 : ℝ) := by
  77  unfold m_c_predicted_via_RS