alpha_match
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.