K_1
plain-language theorem explainer
K_1 fixes the universal one-loop coefficient at 4/3 in the QCD pole-to-MSbar mass conversion, arising directly from the color factor C_F. QCD phenomenologists matching RS mass predictions to PDG pole masses for the top quark cite this constant inside the two-loop expansion. The declaration is a direct assignment of the rational value 4/3 to a real number.
Claim. The one-loop coefficient in the pole-to-MSbar relation satisfies $K_1 = 4/3$, so that $m_ {pole} = m_{MS}(m_{MS}) (1 + (4/3) (alpha_s / pi) + K_2 (alpha_s / pi)^2 + O(alpha_s^3))$ with $N_l = 5$ for the top quark.
background
The module supplies the two-loop conversion between pole and MS-bar quark masses required to compare RS predictions with experimental data. The defining relation is $m_{pole} = m_{MS} (1 + (4/3)(alpha_s/pi) + K_2 (alpha_s/pi)^2 + O(alpha_s^3))$, where the one-loop term is universal and the two-loop coefficient $K_2$ depends on the number of light flavors. Upstream canonical arithmetic objects realize the rational 4/3 as a real number in a realization-independent way.
proof idea
The declaration is a direct definition that assigns the literal value 4/3. No lemmas or tactics are applied; the body consists solely of the constant expression.
why it matters
K_1 supplies the leading term inside the pole_factor definition and its inverse, which are required to prove positivity of the mass conversion for alpha_s in (0, 0.5) and to populate the PoleToMSbarCert structure. It fills the universal one-loop slot in the QCD mass relation used by the downstream certificates m_pole_from_MS_pos_top and pole_factor_pos_top.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.