m_running_at_anchor
plain-language theorem explainer
The theorem shows that the two-loop running quark mass returns exactly to its initial value m_0 when the renormalization scale is set to the anchor value alpha_0. QCD model builders and lattice practitioners cite this identity when matching evolved masses to a common reference scale. The proof is a one-line wrapper that substitutes the anchor ratio lemma and finishes by ring simplification.
Claim. Let $m_0 > 0$, $0 < alpha_0$, and $N_f$ a positive integer. Then the two-loop evolved mass at the reference scale satisfies $m(alpha_0; m_0, N_f) = m_0$, where $m(alpha; m_0, N_f)$ is obtained from the initial mass $m_0$ by integrating the two-loop mass anomalous dimension from $alpha_0$ to $alpha$.
background
The module supplies the MS-bar two-loop quark mass anomalous dimension gamma_m(a) = c_0 a + c_1 a^2 with c_0 = 1 and c_1 = (101 N_c - 10 N_f)/24 - 5/8 C_F. The integrated running mass between scales is expressed via the ratio mass_ratio_two_loop, which multiplies the leading power-law factor by an exponential two-loop correction. The definition m_running simply multiplies the initial mass by this ratio. Upstream, mass_ratio_two_loop_at_anchor establishes that the full ratio equals 1 whenever the two scales coincide, and the m_running definition records the product form.
proof idea
Unfold the definition of m_running to expose the product with mass_ratio_two_loop. Rewrite the ratio at equal arguments by the anchor lemma mass_ratio_two_loop_at_anchor, which itself reduces the leading term to 1. Finish with the ring tactic to obtain the identity.
why it matters
The anchor identity is invoked inside massAnomalousDimensionCert_holds to certify that the two-loop implementation is consistent at the reference point. It supplies the normalization condition required by the differential equation for the running mass and thereby closes one link in the QCD RGE chain used by the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.