MassAnomalousDimensionCert
plain-language theorem explainer
MassAnomalousDimensionCert bundles the normalization and positivity properties required for the two-loop quark-mass running formula in QCD. Researchers verifying renormalization-group consistency of running masses cite the certificate to guarantee that the evolved mass stays positive and recovers the initial value at equal scales. The declaration is a bare structure definition whose fields are later instantiated by direct references to the module's positivity and anchor lemmas.
Claim. A structure certifying that the leading mass anomalous dimension coefficient satisfies $c_0=1$, the two-loop coefficient obeys $c_1(5)>0$, the two-loop mass ratio $m(mu)/m(mu_0)$ is positive whenever the couplings are positive, the ratio equals 1 at equal scales, the running mass is positive, and the running mass equals its initial value at equal scales.
background
In the MS-bar scheme the quark mass anomalous dimension is expanded as gamma_m(a) = c_0 a + c_1 a^2 + O(a^3) with a = alpha_s / pi. The module defines the leading coefficient c_0 := 1 and the two-loop coefficient c_1(N_f) = 67/12 - 5 N_f / 18. The two-loop mass ratio is then given by the product of the leading power-law factor and an exponential correction involving c_1 / b_0. Upstream results establish positivity of b_0(5) and of the leading ratio, which are used to prove the corresponding statements for the full two-loop expression. The local setting is the two-loop solution of the renormalization-group equation for the running quark mass between scales mu and mu_0, with N_f active flavors.
proof idea
The declaration is a structure definition that simply records six propositions. Each field is populated in the downstream theorem massAnomalousDimensionCert_holds by direct reference to the module lemmas c0_eq_one (via rfl), c1_at5_pos, mass_ratio_two_loop_pos, mass_ratio_two_loop_at_anchor, m_running_pos, and m_running_at_anchor.
why it matters
This certificate is instantiated by the theorem massAnomalousDimensionCert_holds, which assembles the individual positivity and anchor lemmas into a single record. It supplies the verified properties needed for any downstream calculation that invokes the two-loop running mass formula in the Recognition Science QCD module. Within the broader framework the result closes the two-loop mass-running block that parallels the alpha_s running already established in the sibling module TwoLoopAlphaS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.