mass_ratio_leading_at_anchor
plain-language theorem explainer
The leading-logarithmic quark mass running ratio equals unity when the renormalization scale matches the reference scale. QCD phenomenologists cite this identity to anchor running quark masses at a common point without correction. The proof is a direct term reduction that substitutes the power definition, cancels the scale ratio, and invokes the base case of real exponentiation.
Claim. Let $0 < alpha_0$ and $N_f$ a natural number. Then the leading-log mass ratio satisfies $(alpha_s(mu)/alpha_s(mu_0))^{c_0 / b_0(N_f)} = 1$ when $mu = mu_0$.
background
The module treats the MS-bar quark mass anomalous dimension at two loops. The leading term of the running mass ratio is defined by the power law mass_ratio_leading(alpha_mu, alpha_mu_0, N_f) = (alpha_mu / alpha_mu_0)^{c0 / b0 N_f}, where c0 = 1 and b0(N_f) is the first beta-function coefficient. This expression comes from integrating the one-loop anomalous dimension gamma_m(a) = c0 a. The module also records the two-loop extension that multiplies by an exponential correction involving c1 and b1.
proof idea
The term proof unfolds the definition of mass_ratio_leading, rewrites the ratio alpha_0 / alpha_0 as 1 via div_self on the positivity hypothesis, and concludes with the identity that any positive real number raised to the power zero equals one.
why it matters
This identity supplies the base case for the two-loop mass ratio at the anchor, which is used directly by mass_ratio_two_loop_at_anchor. It closes the trivial reduction step required to anchor running quark masses consistently with the one-loop leading term in the anomalous-dimension module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.