TopQuarkMassScoreCardCert
plain-language theorem explainer
The TopQuarkMassScoreCardCert structure certifies order-of-magnitude consistency for the top quark structural mass on the phi-ladder by requiring positivity of the prediction, an exact ratio phi^6 to the charm prediction, bounds between 10^4 and 10^6 MeV, and positivity of the PDG reference. Recognition Science mass modelers cite it when checking the rung-21 assignment against the phi^51 scaling. The definition assembles the four field conditions directly from the upstream prediction predicates.
Claim. Structure asserting that the top-quark structural mass prediction $m_t$ satisfies $0 < m_t$, $m_t / m_c = phi^6$, $10^4 < m_t < 10^6$ (in MeV), and that the PDG reference row is positive, where $m_t = phi^{51}/2000000$ and $m_c = phi^{45}/2000000$.
background
In Recognition Science, structural quark masses are placed on the phi-ladder with a fixed yardstick of 1/2000000 MeV. The top quark occupies rung 21 in the UpQuark sector, so its prediction is phi^51 divided by that yardstick; the charm quark at rung 15 yields phi^45 over the same factor. Their ratio is therefore exactly phi^6 by the rung difference of six steps. The module documentation labels this Phase 2 P2-t verification and notes that only broad consistency is claimed against the PDG anchor of 172690 MeV.
proof idea
This is a structure definition that declares four independent propositions as fields. No lemmas or tactics are invoked inside the declaration; each field is later supplied by the corresponding row lemmas (row_top_pos, row_top_charm, row_top_order_MeV, row_pdg_top_positive) when an explicit instance is built.
why it matters
The structure is the direct input to the downstream theorem topQuarkMassScoreCardCert_holds, which proves the structure is inhabited. It completes the Phase 2 scorecard slot for the top quark, confirming the phi-ladder rung and the exact scaling relation that follows from the self-similar fixed point phi. The wide MeV interval leaves open the question of future yardstick refinement while preserving the structural ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.