c1_at5_pos
plain-language theorem explainer
The theorem shows that the two-loop mass anomalous dimension coefficient c1 remains positive when five quark flavors are active. QCD running-mass calculations cite this fact to guarantee that the subleading correction factor in the two-loop mass ratio stays positive. The proof reduces directly to unfolding the explicit rational expression for c1 and confirming the numerical inequality by arithmetic evaluation.
Claim. For five active flavors the two-loop coefficient satisfies $0 < 67/12 - 5N_f/18$ evaluated at $N_f=5$.
background
The module treats the MS-bar quark-mass anomalous dimension to two loops. The coefficient c1(N_f) is defined by the closed rational form 67/12 - 5 N_f /18, which arises once C_F = 4/3 and N_c = 3 are inserted into the standard QCD expression. The companion coefficient c0 is fixed at 1. These enter the two-loop mass ratio formula that multiplies the leading-log factor by an exponential correction proportional to (c1/b0 - c0 b1/b0^2). The upstream definition c1 supplies the explicit expression that the present theorem evaluates at N_f = 5.
proof idea
One-line wrapper that unfolds the definition of c1 at N_f = 5 and applies norm_num to the resulting rational inequality.
why it matters
The result supplies the positivity witness required by the structure MassAnomalousDimensionCert, which in turn certifies that the full two-loop mass ratio remains positive for positive couplings. It therefore closes the positivity leg of the running-mass theorem massAnomalousDimensionCert_holds. Within the Recognition framework the lemma supports the controlled evolution of mass scales that later feed into the phi-ladder mass formula and the Berry creation threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.