mass_ratio_two_loop_at_anchor
plain-language theorem explainer
The two-loop mass ratio for MS-bar quark masses equals one when the renormalization scale matches the anchor scale for any positive alpha_0 and any N_f. QCD phenomenologists and lattice groups cite this identity to normalize heavy-quark masses at a common scale. The proof is a one-line wrapper that unfolds the definition and reduces via the leading-order anchor lemma followed by simplification.
Claim. When the strong coupling at the evaluation scale equals the anchor value, the two-loop corrected ratio of running quark masses satisfies $m(mu)/m(mu_0)=1$ for any number of active flavors $N_f$.
background
The module solves the two-loop RGE for MS-bar quark masses with anomalous dimension gamma_m(a) = c_0 a + c_1 a^2 where c_0 = 1 and c_1 = (101 N_c - 10 N_f)/24 - 5/8 C_F (N_c=3). The mass ratio between scales is m(mu)/m(mu_0) = (alpha_s(mu)/alpha_s(mu_0))^(c_0/b_0) times a two-loop correction factor R. The local setting is the closed-form perturbative solution with positivity and anchor properties proved to interface with alpha_s running.
proof idea
The proof unfolds the definition of the two-loop mass ratio and rewrites using the leading-order anchor lemma at equal scales, after which simplification cancels the correction term to yield one.
why it matters
This anchor identity is invoked inside massAnomalousDimensionCert_holds to certify the full two-loop package and inside m_running_at_anchor to recover the input mass at coincident scales. It supplies the normalization step required for the Recognition Science embedding of QCD running masses, ensuring consistency with the phi-ladder yardstick at fixed points.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.