alphaSAtBottomThreshold
plain-language theorem explainer
Defines the boundary value α_s(m_b) by evaluating the five-flavor one-loop running coupling at the bottom-quark threshold scale. Anyone chaining QCD matching across flavor thresholds cites this as the seed for the n_f=4 branch. The body is a one-line evaluation of the n_f=5 runner at μ = bottom_threshold.scale.
Claim. Let $\alpha_s^{(5)}(\mu)$ be the one-loop strong coupling in the $n_f=5$ region (matched at the top threshold). The bottom-threshold boundary value is $\alpha_s(m_b) := \alpha_s^{(5)}(\mu_b)$ where $\mu_b$ is the bottom flavor-threshold scale ($\approx 4.18\,\mathrm{GeV}$).
background
Item 8 Closure Target builds a precise theorem layer around sub-leading quark mass corrections and the running couplings that enter residual signatures. In that setting the strong coupling is evolved piecewise in active-flavor count $n_f$, with continuity matching at heavy-quark thresholds.
The five-flavor runner alphaS5At is the one-loop $\alpha_s$ in the $n_f=5$ window, seeded at the top threshold and evolved with the five-flavor QCD beta coefficient $b_0(5)$. The bottom threshold object records scale $4.18$, $n_f$ below equal to 4 and above equal to 5. Evaluating the five-flavor runner exactly at that scale supplies the matched boundary value handed to the four-flavor branch.
This is pure RG bookkeeping: no new dynamics, only the interface value $\alpha_s(m_b)$ between the $n_f=5$ and $n_f=4$ segments.
proof idea
Definitional one-liner. The right-hand side applies the already-defined five-flavor runner at the bottom threshold scale: alphaS5At Physics.RG.bottom_threshold.scale. No tactics, no lemmas beyond that evaluation.
why it matters
Feeds alphaS4At, the one-loop $\alpha_s$ in the $n_f=4$ region matched at the bottom threshold, which itself seeds the charm-threshold boundary and the lower-flavor chain. Inside the Item 8 module this coupling ladder is part of the residual and ratio-family infrastructure used to close the open quark sub-leading correction item and make the all-sector generalization falsifiable. It is scaffolding for continuous matching of $\alpha_s$ across flavor thresholds, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.