mass_ratio_leading_at_anchor
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not include the two-loop exponential correction factor.
- Does not extend to three-loop or higher orders.
- Does not fix a specific value of N_f or alpha_0.
- Does not address scheme dependence beyond MS-bar.
Lean usage
rw [mass_ratio_leading_at_anchor alpha_0 N_f h_alpha_pos]formal statement (Lean)
72theorem mass_ratio_leading_at_anchor (alpha_0 : ℝ) (N_f : ℕ)
73 (h_alpha_pos : 0 < alpha_0) :
74 mass_ratio_leading alpha_0 alpha_0 N_f = 1 := by
proof body
Term-mode proof.
75 unfold mass_ratio_leading
76 rw [div_self (ne_of_gt h_alpha_pos)]
77 exact Real.one_rpow _
78