poleToMSbarCert_holds
plain-language theorem explainer
The declaration certifies that the two-loop pole-to-MSbar conversion structure holds for the top quark with K_1 fixed at 4/3 and all required positivity conditions satisfied. QCD phenomenologists comparing experimental pole masses to Recognition Science predictions across quark flavors would cite this result. The proof is a direct term-mode construction that assembles the certificate fields from upstream positivity lemmas.
Claim. The two-loop QCD pole-to-MSbar conversion for five light flavors satisfies $K_1 = 4/3$, $K_2(5) > 0$, the conversion factor is positive for $0 < α_s < 0.5$, and the derived pole mass is positive whenever the input MSbar mass and $α_s$ obey the same bounds.
background
The module supplies 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$ and $K_2 ≈ 11.1 - 1.04 N_l$. For the top quark one takes $N_l = 5$, yielding $K_2 ≈ 5.9$. The certificate structure bundles the fixed $K_1$ value, positivity of $K_2$ at five flavors, positivity of the pole factor, and positivity of the derived pole mass under the perturbative window $0 < α_s < 0.5$ and positive $m_{MS}$. Upstream lemmas establish $K_2(5) > 0$ by direct unfolding and norm_num, together with the corresponding positivity statements for the factor and mass functions.
proof idea
The proof constructs the PoleToMSbarCert structure in term mode. It assigns K_1_eq by reflexivity, K_2_at5_pos by the upstream positivity theorem, pole_factor_pos_lemma by the top-quark factor positivity lemma, and m_pole_pos_lemma by the derived mass positivity lemma that multiplies the MSbar mass by the factor.
why it matters
This theorem closes the certification of the pole-to-MSbar conversion inside the QCD RGE module, allowing RS mass predictions to be compared directly with PDG pole-mass inputs for the top quark. It rests on the two-loop expansion and the positivity results for the conversion functions. The module documentation records zero sorrys and zero axioms, confirming the conversion is fully formalized for use in cross-flavor mass ladders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.