row_top_charm
plain-language theorem explainer
The ratio of the Recognition Science structural top quark mass to the charm quark mass equals exactly phi to the sixth power. Researchers building the top quark mass scorecard cite this result to confirm the 6-rung gap on the phi-ladder. The proof is a one-line wrapper that invokes the upstream top_charm_ratio theorem after unfolding the power definitions.
Claim. Let $m_t = phi^{51}/2000000$ and $m_c = phi^{45}/2000000$ be the structural top and charm quark masses in MeV. Then $m_t/m_c = phi^6$.
background
The module supplies order-of-magnitude rows for the top quark under the phi-ladder construction. Structural masses are defined in the Verification module as top_quark_pred := phi^51 / 2000000 and charm_quark_pred := phi^45 / 2000000, placing the top at rung 21 and charm at rung 15 in the UpQuark sector. The upstream top_charm_ratio theorem states that the top/charm ratio equals phi^6 exactly (6-rung gap).
proof idea
One-line wrapper that applies the top_charm_ratio theorem from Verification after unfolding the two power definitions and simplifying the resulting ratio.
why it matters
This row is assembled into TopQuarkMassScoreCardCert via the topQuarkMassScoreCardCert_holds theorem. It confirms the exact phi^6 scaling between quark states separated by six rungs, consistent with the self-similar fixed point phi. The result supports the partial theorem status for positivity and the wide MeV interval without claiming sub-percent agreement with the PDG anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.