inv_pole_factor_at_zero
plain-language theorem explainer
The theorem establishes that the inverse pole factor for quark mass conversion equals unity at vanishing strong coupling. QCD calculations matching pole masses to MS-bar values invoke this boundary condition in the perturbative limit. The proof is a direct substitution into the two-loop expression followed by algebraic simplification.
Claim. For every natural number $N_l$, the two-loop inverse conversion factor from pole mass to MS-bar mass at zero strong coupling strength equals one: $1 - K_1 (0/π) + (K_1^2 - K_2(N_l)) (0/π)^2 = 1$.
background
This module supplies the two-loop relation between pole and MS-bar quark masses needed to compare RS predictions across flavors. The pole mass satisfies $m_{pole} = m_{MS} · pole_factor(α_s, N_l)$ with the explicit two-loop truncation $1 + (4/3)(α_s/π) + K_2(N_l)(α_s/π)^2 + O(α_s^3)$, while the inverse factor is the truncated series $1 - K_1 (α_s/π) + (K_1^2 - K_2(N_l))(α_s/π)^2$. The upstream definition of the inverse factor supplies the explicit coefficients used here.
proof idea
The proof is a one-line wrapper that unfolds the definition of the inverse pole factor and applies simplification to evaluate the expression at zero strong coupling.
why it matters
This boundary condition normalizes the perturbative expansion for the pole-to-MS-bar conversion, ensuring the leading-order identity holds exactly at zero coupling. It supports the module's master certificate by fixing the constant term in the two-loop truncation. The result aligns with the module status of zero axioms and closes the normalization without reference to higher-order terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.