alphaS3At
plain-language theorem explainer
Defines one-loop α_s(μ) in the three-flavor QCD region by RG-evolving the charm-threshold anchor with b₀(n_f=3). Downstream piecewise α_s stitching cites it as the μ < m_c branch. The body is a pure definitional application of the standard one-loop running formula.
Claim. For any renormalization scale $\mu\in\mathbb{R}$, set $\alpha_s^{(3)}(\mu)$ equal to the one-loop running value with three active flavors, matched at the charm threshold: $\alpha_s^{(3)}(\mu)=\alpha_s(m_c)\big/\bigl(1+\frac{b_0^{(3)}}{2\pi}\,\alpha_s(m_c)\,\ln(\mu/m_c)\bigr)$, where $b_0^{(3)}=11-2\cdot 3/3=9$, $m_c$ is the charm threshold scale, and $\alpha_s(m_c)$ is taken from the four-flavor branch.
background
The module builds a minimal theorem layer aimed at closing Item 8 (quark sub-leading mass corrections) and making the all-sector residual formula falsifiable. Alongside residual-signature algebra it records the QCD running coupling needed when mass formulas are evaluated away from a fixed reference scale.
Upstream, alpha_s_running is the textbook one-loop formula $\alpha_s(\mu)=\alpha_s(\mu_)/(1+b_0/(2\pi),\alpha_s(\mu_),\ln(\mu/\mu_*))$. The coefficient $b_0(n_f)=11-2n_f/3$ encodes asymptotic freedom for $n_f<16.5$. The charm threshold is fixed at scale $1.27$ with $n_f$ stepping from 3 below to 4 above. The anchor alphaSAtCharmThreshold is the value of the $n_f=4$ branch evaluated at that scale, so the three-flavor evolution is continuous across the threshold.
proof idea
Definitional wrapper, not a proof. Instantiates alpha_s_running with four arguments: the charm-threshold anchor alphaSAtCharmThreshold, the three-flavor beta coefficient b0_qcd 3, the free scale $\mu$, and charm_threshold.scale as $\mu_*$. No tactics or lemmas are invoked.
why it matters
Supplies the lowest rung of the piecewise one-loop $\alpha_s$ used in the Item 8 closure target. Downstream, alphaSPiecewise selects alphaS3At μ whenever $\mu$ lies below the charm threshold, after checking top, bottom, and charm cuts in order. That piecewise coupling is the running input against which residual mass corrections and ratio-family predictions can be compared across scales. Within Recognition Science this is bookkeeping infrastructure rather than a forcing-chain step (T0–T8); it keeps the verification layer aligned with standard QCD threshold matching so Item 8 claims remain experimentally checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.