row_anchor_top_charm_ratio_rpow
plain-language theorem explainer
The ratio of anchor masses for the top quark to the charm quark equals phi to the sixth power. Recognition Science mass modelers cite this to confirm phi-ladder rung spacing for up-type fermions with equal Z. The proof rewrites the exponential ratio lemma, invokes the real power definition on positive phi, and applies ring normalization.
Claim. The ratio of the anchor mass for the top quark to the anchor mass for the charm quark equals $phi^6$.
background
The anchor mass function is defined as $M_0$ times the exponential of $((rung f - 8 + gap(ZOf f)) * log phi)$. This module deepens QuarkScoreCard by showing exact agreement on within-family ratios for u/c/t via the equal-Z anchor bridge. The upstream lemma row_anchor_top_charm_ratio_exp establishes the equivalent form exp(6 * log phi) from the rung difference of 6 and ZOf .t = ZOf .c.
proof idea
The proof first rewrites using the exponential ratio lemma row_anchor_top_charm_ratio_exp. It then applies Real.rpow_def_of_pos with phi_pos to convert the exponential, followed by ring_nf to obtain the power form.
why it matters
This supplies the anchor side for the agreement theorem row_top_charm_structural_anchor_agree, which equates the structural prediction ratio to the anchor ratio. It closes one link in the phi-ladder mass formula, consistent with the self-similar fixed point phi and T6. The absolute MeV calibration remains an open residual per the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.