N_f_Z
plain-language theorem explainer
The definition fixes the number of active quark flavors at the Z boson mass scale to five. QCD researchers computing one-loop running of the strong coupling cite this fixed integer when evaluating the beta function coefficient. The declaration is a direct constant assignment with no computation or lemmas involved.
Claim. Let $N_f$ denote the number of active quark flavors at the $Z$ boson mass scale. Then $N_f = 5$.
background
The module treats the running of the strong coupling from Recognition Science, fixing α_s = 2/17 at the Z scale. The one-loop beta function coefficient takes the form b₀ = (11 N_c - 2 N_f)/(12 π) with N_c = 3 colors, which remains positive for N_f below 17 and thereby produces asymptotic freedom. Upstream beta definitions supply only notational conventions for inverse temperature or PPN parameters and are not invoked in the present assignment.
proof idea
The declaration is a direct constant definition that assigns the natural number 5. No lemmas are applied and the body consists solely of the literal integer.
why it matters
This value is substituted into alpha_s_running, the theorem asymptotic_freedom (which proves the beta coefficient positive), and beta0_at_Z (which evaluates b₀ = 23/(12 π)). The module documentation states that the choice keeps N_f below the 17-flavor threshold required for asymptotic freedom in the Recognition Science treatment of QCD running.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.