m_t_MS_at_mt_pos
plain-language theorem explainer
The theorem establishes positivity of the RS-anchored top-quark MS-bar mass evaluated at the top scale, a numerical anchor used when verifying the predicted pole mass against PDG data. Particle physicists and Recognition Science modelers cite it inside the top-quark scorecard to close the positivity chain for the rung-21 sector. The proof is a one-line term wrapper that unfolds the constant 162.5 and applies norm_num.
Claim. The RS-anchored top-quark MS-bar mass at the top-quark scale satisfies $0 < m_{t,MS}(m_t)$ where $m_{t,MS}(m_t) = 162.5$ GeV.
background
The module Top Quark Pole / MS-bar Mass Scorecard records the PDG 2024 pole mass 172.69 ± 0.30 GeV together with the RS assignment of rung t = 21 for the up-type third generation. The constant m_t_MS_at_mt_GeV is defined as the reference MS-bar value 162.5 GeV at the m_t scale with five light flavors. Upstream, the theorem applied records energy conservation H(γ(t1), p(t1)) = H(γ(t2), p(t2)) under time-translation symmetry, while scale(k) := phi^k supplies the phi-ladder scaling used throughout the mass formulas.
proof idea
The proof is a one-line term-mode wrapper. It unfolds m_t_MS_at_mt_GeV to the literal 162.5 and invokes norm_num to discharge the goal 0 < 162.5.
why it matters
The result is invoked by m_t_pole_predicted_pos to obtain 0 < m_t_pole_predicted(alpha) via m_pole_from_MS_pos_top and by topMSBarCert_holds to assemble the full TopMSBarCert record containing rung_eq_21, pdg_pos, and ms_at_mt_pos. It supplies the numerical positivity anchor for the top-quark entry on the phi-ladder at rung 21, consistent with the eight-tick octave and the RS mass formula yardstick * phi^(rung-8+gap(Z)). No scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.