alphaSPiecewise
plain-language theorem explainer
Piecewise one-loop strong coupling α_s(μ) stitched across the charm, bottom, and top flavor thresholds. Quark mass-transport definitions cite it when carrying PDG masses to the RS anchor scale. The body is a four-branch if-cascade selecting the active n_f running formula by comparing μ to the threshold scales.
Claim. For a renormalization scale $\mu\in\mathbb{R}$, the piecewise strong coupling $\alpha_s^{\mathrm{pw}}(\mu)$ equals the six-flavor one-loop value when $\mu$ is at or above the top threshold, the five-flavor value between bottom and top, the four-flavor value between charm and bottom, and the three-flavor value below the charm threshold.
background
Item 8 Closure Target builds the smallest precise theorem layer that would close the open quark sub-leading mass correction and make the all-sector generalization falsifiable. Masses must be compared at a common RS anchor scale, so PDG values are RG-transported with a consistent $\alpha_s$ history.
Heavy-quark thresholds mark where the active flavor count $n_f$ jumps. Upstream, charm_threshold sits at scale $1.27$ ($n_f$: 3 below, 4 above), bottom_threshold at $4.18$ ($n_f$: 4 to 5), and the top threshold likewise steps $n_f$ to 6. Each branch alphaS$n$At is the corresponding one-loop running formula at fixed $n_f$.
The piecewise object is the single continuous-in-scale input that mass transport expects: one function of $\mu$ rather than a manual choice of $n_f$ at each call site.
proof idea
Pure definition, no proof obligations. Nested comparisons against the three heavy-quark threshold scales select which fixed-$n_f$ one-loop runner applies: top and above uses the six-flavor formula, then bottom, then charm, else the three-flavor formula. No algebraic lemmas; the cascade is the entire content.
why it matters
Every anchor-scale quark mass in this module threads through this runner: up, down, strange, charm, bottom, and top masses at the anchor all call transport_mass_through with alphaSPiecewise as the coupling history. Those transported masses feed the residual signatures and refined-family closure targets that Item 8 is built to solve uniquely.
Without a single stitched $\alpha_s$, each sector would carry an ad-hoc $n_f$ choice, breaking comparability of residuals across light and heavy quarks. The definition is scaffolding infrastructure for the LO mass-transport layer, not itself a forcing-chain step (T0–T8), but it is required before residual pairs and $\eta$-refined families can be checked against PDG data at one scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.