c_2_alpha
The definition supplies the next-to-leading-order coefficient for matching the strong coupling alpha_s across heavy-quark flavor thresholds in the MS-bar scheme. QCD phenomenologists cite this constant when evolving couplings between n and n+1 active flavors at the scale mu = m_q^MSbar. It is introduced by direct assignment of the rational 11/72, matching the known perturbative result.
claimThe NLO coefficient $c_2$ in the strong-coupling matching condition at the heavy-quark threshold is $c_2 = 11/72$.
background
The ThresholdMatching module implements NLO matching conditions for alpha_s and quark masses when the number of active flavors changes at heavy-quark thresholds. The coupling matching takes the form alpha_s^{(n)}(mu_q) = alpha_s^{(n+1)}(mu_q) * (1 + c_2 * (alpha_s / pi)^2), with c_2 = 11/72 and mu_q set to m_q^{MSbar}. The mass matching uses the companion coefficient d_2_mass = -89/432 from the sibling definition in the same module.
proof idea
This is a direct definition that assigns the rational number 11/72. No lemmas or tactics are applied; the body is a simple numeric literal.
why it matters in Recognition Science
The constant enters the definition of alpha_match and is referenced by alpha_match_pos, alpha_unmatch, mass_match_pos, and the master certificate ThresholdMatchingCert. It realizes the c_2 term in the module's NLO matching conditions as stated in the module documentation. In the Recognition framework it supplies the perturbative QCD input needed for consistent evolution across thresholds, supporting the interface to the phi-ladder mass formulas.
scope and limits
- Does not derive the coefficient from the Recognition Science forcing chain or functional equation.
- Does not include higher-order O(a^3) or higher terms in the matching expansion.
- Does not specify the renormalization scheme beyond the standard MS-bar convention.
- Does not prove positivity of the matching factor; that is handled separately in c_2_alpha_pos.
Lean usage
def alpha_match (alpha_above : ℝ) : ℝ := alpha_above * (1 + c_2_alpha * (alpha_above / Real.pi) ^ 2)formal statement (Lean)
41def c_2_alpha : ℝ := 11 / 72
proof body
Definition body.
42
43/-- NLO mass matching coefficient at mu = m_q^MSbar.
44 Standard result: d_2_mass = -89/432 (negative; mass slightly decreases). -/