alpha_unmatch
plain-language theorem explainer
alpha_unmatch supplies the NLO inverse matching factor for the QCD strong coupling when descending across a heavy-quark threshold. Phenomenologists running alpha_s in multi-flavor schemes cite this expression when inverting the standard matching relation. The definition is a direct algebraic expansion using the fixed coefficient 11/72.
Claim. The NLO inverse matching applied to the coupling below threshold is given by $a_b (1 - c_2 (a_b / pi)^2)$ where $c_2 = 11/72$ is the standard NLO coefficient.
background
Heavy-quark threshold matching in QCD at NLO relates the strong coupling in n-flavor and (n+1)-flavor theories at the scale mu_q = m_q^MSbar. The module states the forward relation 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. The upstream definition c_2_alpha fixes this coefficient exactly as 11/72.
proof idea
One-line definition that multiplies the input coupling alpha_below by the inverse NLO factor (1 - c_2_alpha * (alpha_below / pi)^2) using the imported coefficient.
why it matters
This definition supplies the structural inverse needed for consistent downward running of alpha_s across flavor thresholds inside the ThresholdMatching module. It supports the master certificate ThresholdMatchingCert by providing the unmatching operation required for NLO QCD evolution. In the Recognition Science setting it contributes to the precise extraction of alpha^-1 inside the predicted interval (137.030, 137.039) by maintaining accurate coupling running.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.