alphaSAtCharmThreshold
plain-language theorem explainer
Defines the strong coupling at the charm threshold, α_s(m_c), by evaluating the four-flavor one-loop running formula at μ = 1.27 GeV. Anyone stitching QCD running across heavy-quark thresholds cites this as the matching value handed from the n_f = 4 branch into the n_f = 3 branch. The body is a one-line evaluation of the n_f = 4 runner at the charm scale.
Claim. Let $\alpha_s^{(4)}(\mu)$ be the one-loop strong coupling in the $n_f=4$ region (matched at the bottom threshold). The boundary value at the charm threshold is $\alpha_s(m_c) := \alpha_s^{(4)}(m_c)$ with $m_c = 1.27\,\mathrm{GeV}$.
background
Item 8 Closure Target builds a precise theorem layer for quark sub-leading mass corrections and the all-sector generalization. Part of that layer is a piecewise one-loop $\alpha_s$ stitched across heavy-quark flavor thresholds, so residual and ratio-family formulas can quote a definite running coupling at each mass scale.
Flavor thresholds are recorded as records with a scale and the active flavor counts above and below. The charm threshold sits at scale $1.27$ GeV with $n_f=3$ below and $n_f=4$ above. The four-flavor runner alphaS4At is itself the one-loop formula matched at the bottom threshold and evolved with the $n_f=4$ beta coefficient $b_0^{\mathrm{QCD}}(4)$.
This definition simply freezes that four-flavor curve at the charm matching point, producing the single real number $\alpha_s(m_c)$ that the three-flavor branch will use as its high-scale anchor.
proof idea
One-line definitional wrapper: evaluate the already-defined four-flavor runner at the charm threshold scale. No tactics, no lemmas beyond the upstream definition of the $n_f=4$ running map and the numeric charm scale $1.27$.
why it matters
Feeds directly into the three-flavor runner, which is defined as one-loop evolution of this boundary value with $b_0^{\mathrm{QCD}}(3)$ down from the charm scale. That piecewise stitch is the coupling backbone for residual signatures and ratio-family coefficients in the Item 8 closure target: without a matched $\alpha_s(m_c)$, the $n_f=3$ sector has no continuous handoff from the heavier-flavor region.
In the broader Recognition stack this is bookkeeping rather than a forcing-chain step (T0–T8), but it is required infrastructure for any falsifiable comparison of predicted quark residuals against PDG running. Downstream, the stitched $\alpha_s$ appears in the module’s residual and refined-family constructions that aim to close the open sub-leading mass item.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.