row_pdg_top_positive
plain-language theorem explainer
The theorem asserts that the PDG reference mass for the top quark is strictly positive. It is cited when constructing the top quark mass scorecard certificate in the Recognition Science masses module. The proof is a one-line wrapper that unfolds the constant definition and applies numerical normalization.
Claim. The PDG reference value satisfies $0 < 172690$ (in MeV).
background
The TopQuarkMassScoreCard module addresses Phase 2 structural mass for the top quark on the φ-ladder. It defines the RS prediction as top_quark_pred = φ^51 / 2,000,000 MeV and anchors to the PDG 2024 center m_t ≈ 172.69 GeV expressed as the constant 172690 MeV. The upstream definition row_pdg_top_MeV supplies this numerical reference without further computation.
proof idea
The proof is a one-line wrapper. It unfolds row_pdg_top_MeV to expose the constant 172690 and applies norm_num to discharge the inequality 0 < 172690.
why it matters
This result supplies the positivity component required by topQuarkMassScoreCardCert_holds, which constructs the certificate instance using pdg_ref_pos := row_pdg_top_positive. It contributes to the partial theorem status for the top quark scorecard on the φ-ladder, confirming the wide MeV interval and exact t/c = φ^6 while leaving absolute mass matching open, consistent with the Recognition framework's order-of-magnitude validation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.