b1
plain-language theorem explainer
The b1 definition supplies the two-loop beta-function coefficient in the MS-bar scheme for SU(3) QCD as an explicit function of active flavors N_f. QCD phenomenologists extending one-loop alpha_s running to two loops would cite this expression when implementing renormalization-group evolution. The definition is realized as a direct arithmetic transcription of the canonical formula without lemmas or hypotheses.
Claim. For the number of active quark flavors $N_f$, the two-loop beta coefficient is $b_1(N_f) = (102 - 38 N_f / 3) / (8 pi^2)$.
background
The module TwoLoopAlphaS extends the one-loop alpha_s running from AlphaRunning to include the second beta-function coefficient, giving the standard MS-bar two-loop formula. The beta function is written d alpha_s / d log mu^2 = -beta0 alpha_s^2 - beta1 alpha_s^3 + O(alpha_s^4), with the canonical SU(3) form beta1 = (102 - 38 N_f / 3) / (8 pi^2) for N_c = 3. Upstream imports supply Real arithmetic, pi, and one-loop structures; the listed depends_on edges bring in foundational classes such as collision-free from OptionAEmpiricalProgram and spin-2 from SpinStatistics, though this definition stands as an algebraic identity.
proof idea
The declaration is a definition whose body is the single arithmetic expression (102 - 38 * (N_f : ℝ) / 3) / (8 * Real.pi ^ 2). No tactics or lemmas are applied; it directly encodes the standard two-loop coefficient.
why it matters
b1 is used by alpha_s_two_loop, alpha_s_two_loop_pos_when_denom_pos, and mass_ratio_two_loop inside the module, and appears in gcicCert, gcic_existence_of_global_phase, and BraakStage downstream. It supplies the missing two-loop term in the Heavy Quark closure track, connecting the alpha inverse band (137.030, 137.039) and phi-ladder mass formulas to the Recognition Science forcing chain. No scaffolding or open questions attach to this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.