massAnomalousDimensionCert_holds
plain-language theorem explainer
The theorem certifies that the two-loop MS-bar quark mass anomalous dimension satisfies c_0 equals one, c_1 at five flavors is positive, and the mass ratio together with the running mass obey strict positivity and unit normalization at equal scales. QCD phenomenologists implementing perturbative mass evolution would cite the result to confirm consistency of the renormalization-group solution. The proof is a term-mode structure construction that supplies reflexivity for the leading coefficient and inserts the pre-proved positivity and anchor le
Claim. The two-loop quark mass anomalous dimension in the MS-bar scheme satisfies $c_0=1$, $0<c_1(N_f=5)$, the two-loop mass ratio is strictly positive for positive strong couplings, equals unity at equal renormalization scales, and the running mass function is positive while recovering the initial mass value at the anchor scale.
background
The module treats the MS-bar quark mass anomalous dimension to two loops. With $a=alpha_s/pi$ the expansion reads $gamma_m(a)=c_0 a + c_1 a^2 + O(a^3)$, where $c_0=1$ sets the leading normalization and $c_1$ takes the standard form $(101 N_c - 10 N_f)/24 - 5/8 C_F$ for $N_c=3$. The two-loop mass ratio is defined as the product of the leading power-law term and an exponential correction linear in the difference of couplings; the running mass is obtained by multiplying an initial mass by this ratio.
proof idea
The proof constructs the MassAnomalousDimensionCert structure in term mode. It supplies rfl for the field c0_eq_one and directly inserts the theorems c1_at5_pos, mass_ratio_two_loop_pos, mass_ratio_two_loop_at_anchor, m_running_pos, and m_running_at_anchor into the remaining fields.
why it matters
The declaration supplies the terminal certified object for the two-loop mass running relations inside the module, confirming that all positivity and normalization conditions required by the renormalization-group solution hold. It assembles the leading-order and two-loop ratio lemmas together with the explicit positivity of c1 at five flavors. Within the Recognition Science setting the result furnishes the QCD input that can be matched to the phi-ladder mass formula at hadronic scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.