row_structural_top_charm_ratio_rpow
plain-language theorem explainer
The theorem states that the ratio of structural top-quark to charm-quark mass predictions equals phi to the sixth power under a real exponent. Researchers deriving quark hierarchies from the Recognition Science phi-ladder cite it to confirm the six-rung separation in the up sector. The proof is a one-line wrapper that lifts the natural-number exponent version via simplification.
Claim. Let $m_t$ be the structural top-quark mass prediction and $m_c$ the charm-quark prediction on the phi-ladder. Then $m_t / m_c = phi^6$.
background
In the Quark Absolute Bridge Score Card module the structural predictions are taken from Verification: charm_quark_pred equals phi raised to 45 divided by 2 000 000, while top_quark_pred equals phi raised to 51 over the same divisor. Their ratio is therefore phi to the sixth. The module proves exact agreement on within-family ratios for the up-sector quarks u/c/t between the structural rs_mass_MeV formula and the anchor massAtAnchor expression. Upstream, row_top_charm_ratio already establishes the same ratio with a natural-number exponent.
proof idea
The proof is a one-line wrapper that applies simpa with the Real.rpow_natCast lemma to the upstream theorem row_top_charm_ratio, converting the natural-number power to a real exponent.
why it matters
The result is invoked directly by row_top_charm_structural_anchor_agree to equate the structural ratio with the corresponding anchor ratio. It completes the P0-Q bridge row for the top/charm structural ratio expressed as a real-power phi law. In the Recognition framework this rests on the self-similar fixed point phi and the eight-tick octave structure of the mass ladder. The absolute MeV bridge remains a partial theorem whose residual divisor mismatch is left explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.