mass_anomalous_dim
plain-language theorem explainer
The definition supplies the constant 8 for the one-loop QCD mass anomalous dimension γ₀, universal for all quarks. QCD renormalization group calculations and Recognition Science running-coupling derivations cite it to obtain the mass evolution exponent γ₀/(2b₀). The implementation is a direct numerical assignment requiring no lemmas or computation.
Claim. The one-loop QCD mass anomalous dimension is defined by $γ_0 := 8$.
background
In the Recognition Science treatment of renormalization group flow, the φ-ladder derivative determines the β-function structure, with the anchor scale μ* = 182.201 GeV as a stationarity point. The mass anomalous dimension γ₀ enters the running quark mass formula through the exponent γ₀/(2b₀), where b₀ is the first coefficient of the QCD β-function. Upstream, Mass is simply the type ℝ and the forcing structure supplies the self-reference axioms that underlie the ladder construction.
proof idea
The definition is a direct constant assignment of the value 8. No lemmas are invoked; the body is a literal numeral that downstream definitions unfold to compute concrete exponents for each n_f.
why it matters
This constant anchors the mass running formulas that feed mass_evolution_exp and the four concrete theorems mass_evo_exp_nf3 through mass_evo_exp_nf6. It connects the φ-ladder derivative of the coupling (from the module setting) to the standard QCD result γ₀ = 8, thereby supporting the derivation of asymptotic freedom for n_f ≤ 16 while preserving the universal one-loop anomalous dimension. It touches the open question of whether the numerical value 8 can be recovered from the RS ladder axioms rather than imported.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.