TopQuarkMassScoreCardCert
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.
claimStructure 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 in Recognition Science
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.
scope and limits
- Does not claim sub-percent numerical match to the PDG value 172690 MeV.
- Does not derive the rung numbers from the base forcing chain.
- Does not extend the claim beyond the interval 10^4 to 10^6 MeV.
- Does not apply to quarks outside the UpQuark sector.
formal statement (Lean)
47structure TopQuarkMassScoreCardCert where
48 positive : 0 < top_quark_pred
49 top_charm : top_quark_pred / charm_quark_pred = phi ^ (6 : ℕ)
50 order_MeV : (10000 : ℝ) < top_quark_pred ∧ top_quark_pred < 1000000
51 pdg_ref_pos : 0 < row_pdg_top_MeV
52