alphaSAtTopThreshold
plain-language theorem explainer
Boundary value α_s(m_t) taken from the one-loop six-flavor QCD running branch, evaluated at the top threshold scale (~172.69 GeV). Downstream five-flavor running anchors on this number for continuous matching across the top threshold. Citation target for anyone wiring the Item 8 RG ladder. Proof shape: one-line evaluation of the n_f=6 runner at the threshold scale.
Claim. Define the boundary value $\alpha_s(m_t)$ as the one-loop strong coupling in the $n_f=6$ region, evaluated at the top-quark flavor threshold scale $\mu_t\approx 172.69\,\mathrm{GeV}$.
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. Among the supporting numerical scaffolding is a matched one-loop $\alpha_s$ ladder across heavy-flavor thresholds.
The six-flavor runner alphaS6At is the one-loop formula anchored at the RS $\alpha_s$ reference point, with $\beta$-function coefficient $b_0$ for $n_f=6$. The top threshold object records scale $172.69$, $n_f$ jumping from 5 below to 6 above. Evaluating the six-flavor branch exactly at that scale supplies the continuous boundary value used when the five-flavor branch takes over below $m_t$.
This sits in ordinary QCD running-coupling bookkeeping, not in the J-cost or phi-ladder mass formula itself; it is infrastructure so residual and ratio-family identities can quote a consistent $\alpha_s(\mu)$ when needed.
proof idea
One-line definitional wrapper: return the six-flavor one-loop runner evaluated at the top threshold scale. No tactics, no lemmas beyond the already-defined runner and the threshold record's scale field.
why it matters
Feeds the five-flavor runner: that definition anchors one-loop $\alpha_s$ in the $n_f=5$ region at this boundary value and evolves with $b_0(n_f=5)$ down from the top threshold. The matched ladder is part of the numerical spine of the Item 8 module (unified sub-leading mass formula), so residual signatures and refined-family solvability statements can refer to a single continuous $\alpha_s$ path across $m_t$.
It does not itself close Item 8; the proved core of the module is structural (ratio-family consistency obstruction, $\eta$ identities, refined-family $\exists!$ per sector). This definition only stabilizes the coupling input those statements may quote. No direct T0–T8 forcing step; pure RG matching support inside Verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.