m_t_pole_predicted_pos
plain-language theorem explainer
The positivity of the RS-predicted top-quark pole mass holds for any strong coupling alpha at the top scale lying in (0, 0.5). QCD phenomenologists comparing the Recognition Science ladder to PDG pole-mass data would cite this result when closing the top-quark scorecard. The argument is a direct one-line wrapper that feeds the fixed RS MS-bar reference and its positivity theorem into the general five-flavor pole-conversion lemma.
Claim. Let $m_t^{MS} = 162.5$ GeV denote the Recognition-Science reference MS-bar mass at the top-quark scale. For every real number $0 < alpha < 0.5$, the pole mass $m_t^{pole}(alpha)$ obtained from the five-flavor QCD conversion formula applied to $m_t^{MS}$ satisfies $0 < m_t^{pole}(alpha)$.
background
The Top Quark Pole / MS-bar Mass Scorecard module anchors the top quark at rung 21 of the phi-ladder and records the PDG 2024 pole-mass central value 172.69 GeV. The reference MS-bar mass is the constant 162.5 GeV. The predicted pole mass is defined by feeding this constant together with the running strong coupling into the two-loop QCD pole-conversion formula with five light flavors. The upstream theorem m_pole_from_MS_pos_top states that the conversion factor remains positive whenever the input MS-bar mass is positive and the coupling lies in (0, 0.5).
proof idea
The proof is a one-line wrapper that applies the theorem m_pole_from_MS_pos_top to the concrete arguments given by the RS MS-bar reference value, the variable alpha_at_mt, and the already-proved positivity statements for the reference mass and the coupling bounds.
why it matters
This result discharges the prediction_pos field inside topMSBarCert_holds, thereby completing the TopMSBarCert structure for rung 21. It supplies the positivity half of the closed RS heavy-quark scorecard that permits direct numerical comparison with the PDG band. The construction sits inside the Recognition Science program that derives quark masses from the phi-ladder fixed point and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.