alpha_match
alpha_match defines the NLO matching factor converting the strong coupling above a heavy-quark threshold to the value below it. QCD phenomenologists running alpha_s across charm or bottom thresholds cite this factor. The definition is a direct algebraic multiplication of the input by one plus the fixed coefficient c_2_alpha times (alpha_above over pi) squared.
claim$alpha_s^{(n)}(mu_q) = alpha_s^{(n+1)}(mu_q) left(1 + frac{11}{72} left(frac{alpha_s^{(n+1)}(mu_q)}{pi}right)^2 right)$ at the heavy-quark threshold scale $mu_q = m_q^{MSbar}$.
background
The module supplies the structural matching infrastructure for QCD couplings and masses when the number of active flavors changes at a heavy-quark threshold. The NLO formula for the coupling is alpha_s^(n)(mu_q) = alpha_s^(n+1)(mu_q) * (1 + sum c_k a^k) with c_1 = 0 and c_2 = 11/72 in the MS-bar scheme at mu_q = m_q. The upstream definition c_2_alpha supplies exactly this coefficient 11/72. The scale function from LargeScaleStructureFromRS supplies the phi-powered energy scales used to locate thresholds in the broader Recognition Science framework.
proof idea
This is a direct one-line definition that multiplies the input alpha_above by the NLO correction factor built from c_2_alpha. No lemmas or tactics are applied; the expression is the complete body.
why it matters in Recognition Science
This definition supplies the core multiplicative factor used by alpha_match_pos to prove positivity and by ThresholdMatchingCert to certify the full set of threshold properties. It implements the NLO term in the heavy-quark decoupling formula stated in the module documentation, ensuring that phi-ladder scales remain consistent with standard QCD running. The construction closes the algebraic part of the threshold infrastructure before any higher-order or numerical extensions.
scope and limits
- Does not include perturbative corrections beyond NLO.
- Does not fix the numerical value of the threshold scale mu_q.
- Does not establish positivity or other analytic properties.
- Does not compute the inverse unmatching factor.
formal statement (Lean)
49def alpha_match (alpha_above : ℝ) : ℝ :=
proof body
Definition body.
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. -/