pith. machine review for the scientific record. sign in
theorem proved wrapper high

beta0QCD_nf0

show as:
view Lean formalization →

The one-loop QCD beta coefficient evaluates to 11 for zero active fermion flavors. Researchers computing mass residues in the Recognition Science framework cite this when initializing the pure-glue running of the strong coupling. The proof is a one-line wrapper that applies norm_num directly to the definition of beta0QCD.

claimThe one-loop QCD beta coefficient in the convention $beta_0 = 11 - (2/3) n_f$ satisfies $beta_0(0) = 11$.

background

The RGTransport module formalizes renormalization group transport for mass residues. It defines the integrated residue $f$ from the mass anomalous dimension $gamma_m$, normalized by $lambda = ln phi$, and relates the structural mass at the anchor scale to the physical mass via the phi-ladder. The upstream definition states that beta0QCD is the one-loop QCD beta coefficient in the convention beta0 = 11 - 2*nf/3.

proof idea

This is a one-line wrapper that applies the norm_num tactic to the definition of beta0QCD.

why it matters in Recognition Science

This supplies the base value for the QCD beta function in the zero-flavor limit, which enters the one-loop running coupling within the RGTransport module. It anchors the leading term in RG transport calculations for structural masses at the phi-ladder anchor, consistent with the mass formula in the Recognition Science framework.

scope and limits

formal statement (Lean)

 126theorem beta0QCD_nf0 : beta0QCD 0 = 11 := by

proof body

One-line wrapper that applies norm_num.

 127  norm_num [beta0QCD]
 128

depends on (1)

Lean names referenced from this declaration's body.