row_pdg_top_MeV
plain-language theorem explainer
The constant 172690 supplies the PDG 2024 central value for the top quark mass in MeV units as a reference anchor. Recognition Science researchers comparing phi-ladder structural predictions to experimental data cite this value inside scorecard certificates. It enters as a direct numeric assignment with no further computation or lemmas required.
Claim. Let $m_t^{PDG} = 172690$ denote the PDG 2024 central value of the top quark mass expressed in MeV.
background
Recognition Science places quark masses on the phi-ladder, where the top quark occupies rung 51 and yields the structural prediction phi to the 51 divided by two million MeV. The module documentation states that this definition anchors the scorecard to the experimental PDG 2024 center of approximately 172.69 GeV, converted to 172690 MeV, and serves only as a reference with no tight match claimed. The local setting is Phase 2 P2-t, which verifies positivity, the exact top-to-charm ratio of phi to the 6, and the wide MeV interval bounds.
proof idea
The declaration is a direct numeric assignment of the integer 172690 to a real number. No lemmas are applied and the proof body is empty.
why it matters
This constant supplies the positivity hypothesis inside the TopQuarkMassScoreCardCert structure, which also records the phi^6 ratio and the (10000, 1000000) MeV interval. It completes the measurement anchor for the top quark scorecard in the P2-t phase, consistent with the phi-ladder construction and the eight-tick octave, while leaving open the question of finer corrections beyond order-of-magnitude agreement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.