PoleToMSbarCert
plain-language theorem explainer
PoleToMSbarCert bundles the fixed one-loop coefficient value 4/3, positivity of the two-loop coefficient at five light flavors, and positivity of the conversion factor and resulting pole mass for strong coupling below 0.5. QCD phenomenologists cite it when mapping experimental pole masses to the MS-bar scheme required by Recognition Science phi-ladder mass formulas. The structure is assembled directly from the module's coefficient definitions and positivity lemmas.
Claim. The certificate asserts that the one-loop coefficient equals $4/3$, the two-loop coefficient at five light flavors is positive, the conversion factor $1 + (4/3) (a/π) + K_2 (a/π)^2$ is positive for $0 < a < 0.5$, and the pole mass obtained by multiplying an MS-bar mass by this factor remains positive under the same conditions on the coupling.
background
The module supplies the two-loop pole-to-MS-bar conversion used to reconcile PDG pole masses with the MS-bar scheme appearing in Recognition Science mass predictions. The conversion factor is defined as $1 + (4/3)(α_s/π) + K_2(N_l)(α_s/π)^2$, where the one-loop coefficient is the universal $4/3$ from $C_F$ and the two-loop coefficient is the linear function $K_2(N_l) = 11.1 - 1.04 N_l$. For the top quark the module fixes $N_l = 5$, yielding a positive $K_2$ value proved by direct evaluation.
proof idea
The declaration is a structure definition whose four fields simply record the required equality and three inequalities. No tactics are executed inside the structure itself; the fields are populated by direct reference to the sibling definitions of the coefficients and the separate positivity lemmas for the factor and the mass conversion.
why it matters
The certificate is instantiated by poleToMSbarCert_holds to supply a single object that downstream scorecards can invoke to guarantee positivity of the mass conversion. It supplies the algebraic and sign facts needed to place experimental top-quark data onto the phi-ladder without introducing extra hypotheses. The module documentation states that the entire file contains zero sorrys, confirming the two-loop identities close within the stated perturbative window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.