c0
plain-language theorem explainer
The leading coefficient in the two-loop quark mass anomalous dimension is defined to equal 1. QCD calculations of running masses between renormalization scales cite this universal normalization. The definition consists of a direct constant assignment with no computation.
Claim. The leading coefficient in the expansion of the quark mass anomalous dimension satisfies $c_0 = 1$.
background
The module treats the MS-bar quark mass anomalous dimension to two loops. With $a = alpha_s / pi$, the expansion begins with the term $c_0 a$ where the leading coefficient is universal and sets the overall normalization. The module doc states: 'c_0 = 1 (universal, sets normalization)'. Upstream modules fix the number of colors at 3 and supply canonical arithmetic objects used for invariant content across realizations.
proof idea
The declaration is a direct definition that assigns the real number 1. No lemmas or tactics are applied.
why it matters
This normalization constant enters the integrated solution for the running mass ratio $m(mu)/m(mu_0) = (alpha_s(mu)/alpha_s(mu_0))^{c_0 / b0} times a two-loop correction factor. It feeds the Poisson plateau constructions in the Riemann hypothesis certificate window, where the constant 1 serves as the base scaling for convolution bounds. The choice aligns with the alpha_s running chain in the QCD RGE sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.