alphaS6At
plain-language theorem explainer
One-loop strong coupling α_s(μ) on the six-flavor branch, anchored at the RS scale μ*. Anyone building the piecewise RG stitch across heavy-quark thresholds cites this. The body is a thin wrapper of the standard one-loop running formula with the n_f=6 QCD beta coefficient.
Claim. Define $\alpha_s^{(6)}(\mu)$ as the one-loop running strong coupling with $n_f=6$ active flavors: start from the RS anchor value $\alpha_s(\mu^*)$ and evolve to scale $\mu$ with the one-loop QCD coefficient $b_0^{\mathrm{QCD}}(6)$.
background
Item 8 of the verification stack concerns the open quark sub-leading mass correction. Closing it needs a falsifiable all-sector mass formula, which in turn needs a controlled running of $\alpha_s$ across heavy-quark thresholds so residual signatures can be compared at a common scale.
The one-loop RG formula alpha_s_running evolves an anchor coupling with a fixed $b_0$ coefficient. Here $b_0^{\mathrm{QCD}}(6)$ is the standard six-flavor QCD coefficient; the anchor is the RS-native $\alpha_s(\mu^*)$ at the RS anchor scale. Above the top threshold only six flavors are active, so this branch is the ultraviolet piece of the stitch.
The module already proves structural rigidity and unique refined-family coefficients for residual pairs; the coupling infrastructure supplies the scale dependence those residuals sit on.
proof idea
Pure definition, not a theorem. It specializes Physics.RG.alpha_s_running to the RS anchor coupling, the six-flavor beta coefficient b0_qcd 6, the free scale $\mu$, and the RS anchor scale. No tactics or lemmas beyond that specialization.
why it matters
Feeds two immediate parents in the same module: alphaSAtTopThreshold (the boundary value $\alpha_s(m_t)$ read off this branch) and alphaSPiecewise (the if-then stitch that uses this definition whenever $\mu$ sits at or above the top threshold). Without a named six-flavor branch, the piecewise running cannot match continuously onto the $n_f=5$ segment, and Item 8 residual comparisons lose a common RG frame.
In the broader RS picture this is infrastructure, not a forcing-chain step: it does not touch T5–T8 or the RCL. It supports the verification claim that quark sub-leading corrections can be stated and falsified once running is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.