mass_evo_exp_nf5
plain-language theorem explainer
The mass evolution exponent for five active quark flavors evaluates to 8/(46/3) in the one-loop QCD approximation. Researchers computing running quark masses under the renormalization group in the Standard Model would cite this explicit case. The proof is a one-line wrapper that unfolds the mass evolution exponent, anomalous dimension, and beta coefficient definitions then applies numerical simplification.
Claim. For five active quark flavors the mass evolution exponent equals $8/(46/3)$, where the exponent is defined as the ratio of the one-loop mass anomalous dimension to twice the one-loop QCD beta-function coefficient.
background
The module derives renormalization group flows from the RS phi-ladder, with the beta function sign fixed by the ladder derivative and asymptotic freedom following from the SU(3) color structure. The RS anchor scale is identified as a stationarity point of the flow at 182.201 GeV. Upstream, b0_qcd(n_f) is defined as 11 - 2 n_f / 3, the one-loop coefficient whose positivity for n_f < 16.5 enforces asymptotic freedom; mass_anomalous_dim is the constant 8; and mass_evolution_exp(n_f) is their ratio mass_anomalous_dim / (2 * b0_qcd n_f).
proof idea
One-line wrapper that unfolds mass_evolution_exp, mass_anomalous_dim, and b0_qcd then applies norm_num to obtain the concrete value for n_f = 5.
why it matters
This supplies the concrete n_f = 5 instance of the general mass evolution exponent used in running-mass calculations within the RS renormalization group treatment. It instantiates the beta_function_structure and asymptotic_freedom results of the module for the flavor count relevant to light quarks below the top threshold. No downstream theorems are recorded yet, leaving open its insertion into explicit running-mass formulas at the RS anchor scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.