alphaS4At
plain-language theorem explainer
One-loop strong coupling α_s(μ) in the four active-flavor window, RG-evolved from the bottom-quark threshold with the n_f=4 beta coefficient. Anyone building the piecewise α_s curve across heavy-quark thresholds cites this branch. The body is a thin definitional wrapper around the shared one-loop running formula.
Claim. For a renormalization scale $\mu\in\mathbb{R}$, $\alpha_s^{(4)}(\mu)$ is the one-loop running of the strong coupling with $n_f=4$ active flavors, matched to the boundary value at the bottom-quark mass threshold and evolved with the corresponding one-loop QCD beta coefficient $b_0(n_f=4)$.
background
The host module builds the smallest precise theorem layer that would close Item 8 (open quark sub-leading mass corrections) and make the all-sector generalization falsifiable. Alongside residual-signature algebra and refined-family uniqueness, it needs a concrete running strong coupling so mass-ratio predictions can be evaluated at the right scale.
In the RS/Physics RG layer, one-loop $\alpha_s$ is evolved by alpha_s_running from a matched boundary value with beta coefficient b0_qcd n_f. The bottom threshold supplies the matching scale and the seed value for the $n_f=4$ branch (just below the bottom quark, four light flavors remain active). The golden-ratio ladder and forcing-chain landmarks are ambient framework context; this definition itself is pure QCD running infrastructure.
proof idea
Definitional, not a proof. The body applies the shared one-loop runner Physics.RG.alpha_s_running to four fixed inputs: the matched boundary value at the bottom threshold, the one-loop coefficient b0_qcd 4, the evaluation scale $\mu$, and the bottom-threshold reference scale. No tactics or lemmas beyond that application.
why it matters
Supplies the $n_f=4$ segment of the stitched coupling used in Item 8 verification. Downstream, alphaSAtCharmThreshold evaluates this branch at the charm threshold to seed the three-flavor region, and alphaSPiecewise dispatches to it whenever $\mu$ lies between the charm and bottom thresholds. Without a clean four-flavor branch, the piecewise $\alpha_s$ curve (and any scale-dependent residual or mass-ratio check that depends on it) cannot be stated. This is supporting infrastructure for the Item 8 closure target, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.