inv_pole_factor
plain-language theorem explainer
The definition supplies the explicit two-loop perturbative inverse of the pole-to-MS-bar mass conversion factor. QCD phenomenologists converting the PDG top-quark pole mass to the MS-bar scheme at its own scale would cite this expression when feeding RS mass predictions. It is obtained by direct algebraic truncation of the series inversion of the forward factor at order alpha_s squared.
Claim. The two-loop inverse conversion factor is defined by $1 - (4/3) (alpha_s / pi) + ((4/3)^2 - K_2(N_l)) (alpha_s / pi)^2$, where $K_2(N_l) = 11.1 - 1.04 N_l$.
background
In the Recognition Science treatment of quark masses the pole mass and MS-bar mass are related by a perturbative series in the strong coupling. The forward conversion reads m_pole = m_MS * (1 + (4/3)(alpha_s/pi) + K_2 (alpha_s/pi)^2 + O(alpha_s^3)), with K_1 = 4/3 the universal one-loop coefficient from C_F and K_2(N_l) = 11.1 - 1.04 N_l the two-loop coefficient. The inverse direction is required to translate the experimental pole mass into the scheme used for RS predictions on the phi-ladder. K_1 and K_2 are the only referenced constants; both are defined as ordinary real numbers inside the same module.
proof idea
The definition is the explicit algebraic truncation of the perturbative inverse series. It substitutes the known constants K_1 = 4/3 and K_2(N_l) directly into the closed-form expression 1 - K_1 x + (K_1^2 - K_2) x^2 with x = alpha_s / pi.
why it matters
This definition is used to construct m_MS_from_pole, which converts the PDG pole mass into the MS-bar value needed for RS mass-ladder comparisons across quarks. It closes the two-loop conversion loop begun by pole_factor and K_2. Within the broader framework the expression supports consistent placement of quark masses on the phi-ladder by ensuring scheme-independent inputs to the mass formula yardstick * phi^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.