row_top_charm_ratio
plain-language theorem explainer
The structural top-quark mass divided by the structural charm-quark mass equals phi to the sixth power exactly. A physicist deriving masses on the Recognition Science phi-ladder cites this as the P0-Q06 row in the quark scorecard. The proof is a one-line wrapper that invokes the ratio theorem already established in the Verification module.
Claim. $m_t / m_c = phi^6$, where $m_t$ is the structural top-quark mass prediction at rung 21 and $m_c$ is the structural charm-quark mass prediction at rung 15.
background
The Quark Score Card module consolidates Phase 0 rows P0-Q01 through P0-Q06 for the quark sector. Structural masses for up-type quarks are defined as phi raised to a rung-dependent exponent divided by two million. The top quark occupies rung 21 and the charm quark rung 15, producing a six-rung gap on the ladder. Upstream Verification states: 'The top/charm ratio equals φ^6 exactly (6-rung gap).' This row records the ratio as theorem-grade while leaving absolute mass matching open.
proof idea
The proof is a one-line wrapper that applies the top_charm_ratio theorem from the Verification module. That theorem unfolds the definitions of top_quark_pred and charm_quark_pred, then cancels the common denominator and base factors via field simplification.
why it matters
This theorem supplies the top/charm ratio entry inside QuarkScoreCardCert_holds and is invoked by row_structural_top_charm_ratio_rpow in the absolute bridge scorecard. It realizes the six-rung spacing required by the Recognition Science mass formula (yardstick times phi to the rung offset) and closes the P0-Q06 structural row. The open question it touches is the missing gap(ZOf) correction needed for absolute PDG-band matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.