mass_evo_exp_nf4
plain-language theorem explainer
The mass evolution exponent for four active quark flavors equals exactly 8/(50/3). QCD phenomenologists evolving quark masses at low flavor counts would cite this explicit value. The proof is a one-line wrapper that unfolds the exponent definition, the constant anomalous dimension and the beta coefficient then normalizes the resulting arithmetic.
Claim. For four active quark flavors the mass evolution exponent satisfies $8/(50/3)$, where the one-loop anomalous dimension is the constant 8 and the beta-function coefficient is $11-2n_f/3$.
background
The module treats renormalization-group flow inside Recognition Science by anchoring the scale at 182.201 GeV and deriving the beta function from the phi-ladder derivative. The one-loop QCD coefficient is defined by b0_qcd(n_f) = 11 - 2 n_f / 3, which is positive for n_f < 16.5 and thereby enforces asymptotic freedom. The mass anomalous dimension is the universal constant 8, so the evolution exponent is their ratio gamma_0 / (2 b_0).
proof idea
The proof is a one-line wrapper. It unfolds mass_evolution_exp, mass_anomalous_dim and b0_qcd, then applies norm_num to reduce the concrete expression at n_f = 4.
why it matters
The declaration supplies the explicit four-flavor case of the mass evolution exponent that appears in the module's running-coupling formulas. It supports the listed results on asymptotic freedom for n_f <= 16 and the one-loop alpha_s running, all derived from the phi-ladder structure of the beta function. No downstream uses are recorded, so the result functions as a concrete numerical anchor rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.