m_b_predicted_pos
plain-language theorem explainer
The positivity of the two-loop QCD running prediction for the bottom quark MS-bar mass at its own scale, given positive strong couplings at that scale and at MZ. Particle physicists checking heavy-quark mass consistency in the Recognition Science framework cite this result. The proof is a direct one-line wrapper that invokes the general positivity theorem for the two-loop mass evolution function.
Claim. Let $0 < α_b$ and $0 < α_Z$ be the strong coupling values at the bottom-quark scale and at the Z-boson scale. Then the two-loop evolved bottom-quark mass prediction $m_b^pred(α_b, α_Z) > 0$.
background
The Bottom Quark MS-bar Mass Scorecard module implements the Recognition Science assignment of the bottom quark to rung 21 on the phi-ladder, using the PDG 2024 central value 4.18 GeV as reference. The prediction is obtained by two-loop running of the mass from the Z scale down to the bottom scale with five active flavors. The upstream theorem m_b_at_MZ_pos supplies the required positivity of the initial mass at MZ. The general m_running_pos result from the QCD RGE module guarantees that the evolved mass remains positive whenever the initial mass and both couplings are positive.
proof idea
One-line wrapper that applies m_running_pos to the concrete arguments m_b_at_MZ_GeV, alpha_at_mb, alpha_at_MZ and N_f = 5, substituting the already-established positivity of m_b_at_MZ_GeV together with the two given positive coupling hypotheses.
why it matters
This theorem supplies the positivity ingredient required by bottomMSBarCert_holds, which certifies that the RS rung-21 prediction lies inside the PDG band for the bottom quark. It therefore closes the positivity check for the third-generation down-type quark inside the Recognition Science heavy-quark scorecard.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.