alphaS5At
plain-language theorem explainer
Defines the one-loop strong coupling α_s(μ) on the five-flavor branch, evolved from the top-threshold match with the QCD beta coefficient b0(n_f=5). Anyone building a piecewise α_s across heavy-quark thresholds cites this as the middle segment. The body is a direct application of the RG runner at the top scale.
Claim. For a renormalization scale $\mu\in\mathbb{R}$, $\alpha_s^{(5)}(\mu)$ is the one-loop running of the strong coupling with $n_f=5$ active flavors, started from the matched value at the top-quark threshold and evolved with the five-flavor QCD coefficient $b_0(5)$.
background
Item 8 Closure Target builds the smallest precise framework that would close the open quark sub-leading mass correction and make the all-sector generalization falsifiable. Alongside residual signatures and refined ratio families, the module stitches a piecewise one-loop $\alpha_s$ across heavy-quark thresholds so mass-ladder and coupling data can be compared in one place.
The runner alpha_s_running implements standard one-loop QCD evolution of $\alpha_s$ between two scales given a reference value and a $b_0(n_f)$ coefficient. Here the reference is the already-matched top-threshold value, and $b_0$ is taken at five active flavors. The top threshold scale is the matching point that seeds this branch; the bottom threshold later samples this function to seed the $n_f=4$ branch.
In RS-native units the same ladder and threshold scales appear elsewhere (phi-powers, mass yardsticks), but this definition is pure RG bookkeeping: it does not yet encode the Recognition Composition Law or the T5–T8 forcing chain.
proof idea
Definitional wrapper, not a proof. It instantiates the one-loop runner with four arguments: the matched $\alpha_s$ at the top threshold, $b_0^{\mathrm{QCD}}(5)$, the evaluation scale $\mu$, and the top-threshold scale as the evolution origin. No tactics or lemmas beyond that application.
why it matters
Feeds two local consumers: the bottom-threshold boundary value $\alpha_s(m_b)$ sampled from this five-flavor branch, and the piecewise $\alpha_s(\mu)$ that switches among $n_f=6,5,4,3$ at top, bottom, and charm thresholds. That piecewise coupling is infrastructure for Item 8 closure: comparing predicted quark residuals and ratio-family coefficients against running $\alpha_s$ in each flavor window.
It does not itself discharge Item 8. The module’s proved core is structural (consistency of the sign-split family, unique refined $(c,\eta)$ per sector). This definition only supplies the coupling side of the comparison surface. Framework landmarks (T5 $J$-uniqueness, $\phi$, eight-tick octave) are upstream context for why thresholds and ladders matter; they are not invoked in the body.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.