b0_qcd
plain-language theorem explainer
The definition supplies the standard one-loop QCD beta-function coefficient b0 as 11 minus two-thirds times the number of active quark flavors. Particle physicists checking asymptotic freedom conditions in QCD cite this when verifying the sign of the beta function for given flavor counts. It is introduced as a direct arithmetic expression with no lemmas or reductions required.
Claim. The one-loop coefficient in the QCD beta function is $b_0(n_f) = 11 - (2/3)n_f$, where $n_f$ denotes the number of active quark flavors. Asymptotic freedom requires $b_0 > 0$, i.e., $n_f < 16.5$.
background
In the Recognition Science treatment of renormalization group flow, the running of the strong coupling follows from the phi-ladder derivative of the coupling. The module states that the beta-function structure is given by β(g) = (1/ln φ) dg/dr, with the sign of β_QCD fixed by the SU(3) color structure forced by Q3. The RS anchor scale is placed at μ* = 182.201 GeV as a stationarity point of the RG flow.
proof idea
This is a direct definition written as the arithmetic expression 11 - 2*n_f/3 in real numbers. No lemmas are invoked and no tactics are applied beyond the explicit formula.
why it matters
The definition anchors every running-coupling result in the module. It is invoked in asymptotic_freedom_criterion to establish that asymptotic freedom holds for n_f ≤ 16, in b0_sm_positive for the Standard Model case n_f = 6, and in the mass_evolution_exp theorems for n_f = 3 to 6. It encodes the positive b0 produced by the SU(3) structure that the framework derives from the phi-ladder, consistent with the eight-tick octave and D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.