TopMSBarCert
plain-language theorem explainer
The TopMSBarCert structure records the RS rung assignment for the top quark, the PDG 2024 central pole mass, positivity of both pole and MS-bar values, and a positivity guarantee on the predicted pole mass for alpha_s in (0, 0.5). Particle physicists matching RS mass ladders to experimental top data would cite this certificate as the verified input bundle. It is realized directly as a structure definition that assembles the numerical constants and the universal quantification without further lemmas.
Claim. Let $r_t = 21$, let $m_t^{pole, PDG} = 172.69$ GeV satisfy $m_t^{pole, PDG} > 0$, let $m_t^{MS}(m_t) > 0$, and let the predicted pole mass satisfy $m_t^{pole, pred}(α_s) > 0$ for every $α_s ∈ (0, 0.5)$.
background
The Top Quark Pole / MS-bar Mass Scorecard module supplies the RS-anchored inputs for the heaviest quark, with rung 21 assigned to the up-type third-generation state. It imports the two-loop alpha_s running and pole-to-MSbar conversion routines to link the RS mass formula to PDG data. Key definitions are r_top := 21, m_t_pole_PDG_GeV := 172.69, m_t_MS_at_mt_GeV := 162.5, and m_t_pole_predicted α := m_pole_from_MS m_t_MS_at_mt_GeV α 5, which performs the closed heavy-quark conversion at the top scale with five light flavors.
proof idea
TopMSBarCert is a structure definition whose five fields are declared directly. No tactics or upstream lemmas are invoked inside the declaration itself; the fields are later instantiated by the downstream theorem topMSBarCert_holds using reflexivity on the equalities and the positivity statements already proved for the numerical constants.
why it matters
This structure supplies the certified data bundle consumed by topMSBarCert_holds, which witnesses consistency between the RS rung-21 top mass and the PDG 2024 central value. It completes the scorecard for the top quark in the RS mass formula (yardstick times phi to the power rung minus 8 plus gap(Z)), where rung 21 is fixed for the top. The module records zero sorry and zero axiom, confirming the entire top scorecard rests on the imported QCD RGE machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.