topQuarkMassScoreCardCert_holds
plain-language theorem explainer
The declaration certifies existence of a scorecard for the top quark structural mass under the phi-ladder. Researchers checking quark mass hierarchies in Recognition Science cite this when verifying the phi^6 ratio to charm and the 10^4 to 10^6 MeV window. The term proof assembles the certificate structure from four row theorems establishing positivity, the ratio, the bounds, and PDG reference positivity.
Claim. Existence of a certificate $C$ such that $0 < m_t$, $m_t / m_c = phi^6$, $10000 < m_t < 1000000$ (in MeV), and $0 < m_t^{PDG}$, where $m_t$ is the RS phi-ladder prediction for the top quark mass.
background
The module treats Phase 2 P2-t for top quark structural mass on the phi-ladder. The RS prediction is defined as top_quark_pred = phi^51 / 2000000 MeV, with the PDG 2024 center 172690 MeV serving only as reference. The certificate structure TopQuarkMassScoreCardCert requires four properties: positivity of the prediction, the exact ratio top_quark_pred / charm_quark_pred = phi^6, the order-of-magnitude interval 10000 < top_quark_pred < 1000000, and positivity of the PDG reference value in MeV.
proof idea
Term-mode construction that directly populates the certificate structure. It supplies row_top_pos for the positive field, row_top_charm for the top_charm field, row_top_order_MeV for the order_MeV field, and row_pdg_top_positive for the pdg_ref_pos field.
why it matters
This result certifies the partial theorem for the top quark in the Recognition Science mass framework, confirming positivity, the exact phi^6 ratio to charm, and the broad MeV interval required by the phi-ladder mass formula. It aligns with the T6 self-similar fixed point and the yardstick * phi^(rung-8+gap) construction. The module status leaves open refinement to sub-percent numerical agreement with PDG data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.