m_t_pole_PDG_pos
plain-language theorem explainer
The theorem establishes that the PDG central value for the top quark pole mass equals 172.69 GeV and is therefore strictly positive. Particle physicists assembling Recognition Science mass certificates for the top quark would cite this result when verifying the positivity field of the TopMSBarCert structure. The proof is a one-line wrapper that unfolds the constant definition and applies norm_num to confirm the numerical inequality.
Claim. Let $m_t^{pole,PDG}=172.69$ GeV be the central value reported by PDG 2024 for the top quark pole mass. Then $0<m_t^{pole,PDG}$.
background
The module presents a scorecard for the top quark pole and MS-bar masses, taking the PDG 2024 central value 172.69 GeV as input data and associating it with rung t=21 in the RS sector for up-type third-generation quarks. The upstream definition supplies this exact numerical constant as a real number. The positivity statement is required to populate the certificate structure that records agreement between the reported value and the RS ladder prediction.
proof idea
The proof unfolds the definition of the mass constant to the literal value 172.69 and invokes norm_num to discharge the strict inequality by direct numerical comparison.
why it matters
The result supplies the pdg_pos field inside topMSBarCert_holds, which constructs the full TopMSBarCert record containing rung equality, central value, and positivity checks. It anchors the numerical input for the top quark (rung 21) in the Recognition Science mass formula, where the eight-tick octave and phi-ladder fix the rung assignments. The module reports zero sorrys and zero axioms, treating the PDG datum as an external experimental anchor rather than a derived quantity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.