mass_evo_exp_nf3
plain-language theorem explainer
The theorem establishes that the mass evolution exponent for three active quark flavors equals 8/18. Particle physicists computing scale dependence of light quark masses below the charm threshold would cite this concrete value. The proof is a one-line wrapper that unfolds the mass evolution exponent definition, the anomalous dimension, and the beta coefficient then reduces the arithmetic via norm_num.
Claim. For three active quark flavors the one-loop mass evolution exponent equals $8/18$.
background
The module treats renormalization group flows derived from the Recognition Science φ-ladder. The one-loop QCD β-function coefficient is b₀(n_f) = 11 - 2n_f/3, which fixes the sign of the beta function and asymptotic freedom for n_f < 16.5. The mass anomalous dimension is fixed at γ₀ = 8 for all quarks at one loop. The mass evolution exponent is then defined as γ₀ / (2 b₀(n_f)), giving the power-law scaling of quark masses under changes of renormalization scale.
proof idea
The proof is a one-line wrapper. It unfolds mass_evolution_exp to mass_anomalous_dim / (2 * b0_qcd 3), then unfolds mass_anomalous_dim to the constant 8 and b0_qcd 3 to 11 - 23/3 = 9. The norm_num tactic reduces the resulting rational expression 8/(29) directly to 8/18.
why it matters
This supplies the numerical value required for mass running in the three-flavor regime of QCD, which applies below the charm threshold. It supports the module's treatment of asymptotic freedom and the running of α_s anchored at the RS scale. The result instantiates the general mass_evolution_exp definition, which rests on b0_qcd derived from the SU(3) color structure forced by the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.