mass_anomalous_dim_pos
plain-language theorem explainer
The declaration proves positivity of the one-loop QCD mass anomalous dimension. Researchers deriving quark mass running under the renormalization group in QCD cite this when constructing evolution exponents. The proof is a one-line wrapper that unfolds the constant definition and applies norm_num to verify the inequality.
Claim. $0 < 8$ where $8$ is the universal one-loop QCD mass anomalous dimension.
background
The module derives renormalization group flows from the RS φ-ladder, with the anchor scale μ* = 182.201 GeV as a stationarity point and the β-function sign fixed by the ladder derivative of the coupling. The upstream definition supplies the constant value used for mass evolution: One-loop QCD mass anomalous dimension: γ₀ = 8 (universal for all quarks). This constant enters the exponent γ₀/(2b₀) that governs how quark masses scale with the renormalization point.
proof idea
The proof is a one-line wrapper that unfolds the definition of mass_anomalous_dim to expose the constant 8 and then applies norm_num to confirm the strict inequality over the reals.
why it matters
This result supplies the positivity hypothesis required by the downstream theorem mass_evolution_exp_pos, which shows the mass evolution exponent stays positive for n_f ≤ 16. It supports the module's asymptotic freedom criterion and the broader claim that the β-function sign follows from the φ-ladder derivative. The constant 8 is taken as the standard one-loop QCD value and is not re-derived inside the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.