K_2
plain-language theorem explainer
K_2 supplies the two-loop coefficient in the QCD pole-to-MSbar mass conversion as the linear expression 11.1 minus 1.04 times the number of light flavors. QCD phenomenologists converting experimental pole masses to running MSbar values, particularly for the top quark at N_l=5, would cite this closed form. The declaration is a direct arithmetic definition with no lemmas or reductions.
Claim. $K_2(N_l) = 11.1 - 1.04 N_l$, where $N_l$ denotes the number of light quark flavors.
background
The module establishes the two-loop relation $m_{pole} = m_{MS}(m_{MS}) (1 + (4/3) (α_s/π) + K_2 (α_s/π)^2 + O(α_s^3))$ with $C_F = 4/3$. K_1 is fixed at 4/3 while K_2 is the N_l-dependent coefficient. Upstream, pole_factor composes the full conversion factor as 1 + K_1 (α_s/π) + K_2 N_l (α_s/π)^2. The local setting is perturbative QCD mass matching for RS predictions across quark flavors, with canonical N_l=5 for the top.
proof idea
One-line definition that directly assigns the arithmetic expression 11.1 - 1.04 N_l to the real-valued function of N_l.
why it matters
K_2 feeds pole_factor, inv_pole_factor, K_2_at5_pos, pole_factor_pos_top, and the PoleToMSbarCert structure. It supplies the numerical input required for two-loop accuracy in the mass conversion chain, allowing RS mass ladder predictions to be compared with PDG pole masses. The module records zero sorries, confirming the closed form is fully available for downstream positivity and inversion results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.