K_2_at5_pos
plain-language theorem explainer
K_2_at5_pos proves that the two-loop pole-to-MSbar coefficient at five light flavors is positive. QCD mass-conversion calculations in Recognition Science would cite it when assembling the top-quark certificate. The proof is a one-line wrapper that unfolds the explicit definition of K_2 and normalizes the resulting arithmetic inequality.
Claim. $0 < K_2(5)$ where $K_2(N_l) := 11.1 - 1.04 N_l$.
background
The module supplies the two-loop relation between pole mass and MS-bar mass: $m_ pole = m_MS (1 + (4/3)(a/π) + K_2 (a/π)^2 + O(a^3))$, with $K_2(N_l) = 11.1 - 1.04 N_l$ and $N_l$ the number of light flavors. For the top quark one takes $N_l = 5$, giving $K_2(5) ≈ 5.9$. The definition appears as a sibling in the same file and is referenced by the certificate structure that collects the positivity and inversion lemmas needed for Recognition Science mass comparisons.
proof idea
The proof is a one-line wrapper: unfold K_2 followed by norm_num, which reduces the claim to the concrete numerical inequality 0 < 11.1 - 1.04 * 5.
why it matters
The result is required by the PoleToMSbarCert structure (instantiated in poleToMSbarCert_holds) to guarantee that the conversion factor stays positive for small alpha_s at the top-quark scale. It closes the two-loop positivity step in the pole-to-MSbar conversion used by downstream Recognition Science mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.