row_anchor_charm_up_ratio_rpow
plain-language theorem explainer
The theorem establishes that the ratio of anchor masses for the charm quark to the up quark equals phi to the power 11. Researchers verifying quark mass ratios in the Recognition Science phi-ladder would cite this when confirming exact agreement between structural predictions and anchor formulas. The proof rewrites the ratio into its exponential form, applies the real-power definition, and simplifies algebraically.
Claim. Let $m_f$ denote the anchor mass of fermion $f$, defined by $m_f = M_0$ exp$(((rung(f) - 8 + gap(Z(f))) log phi))$. Then $m_c / m_u = phi^{11}$.
background
This declaration belongs to the Quark Absolute Bridge Score Card module, which deepens the QuarkScoreCard by showing that equal-Z anchor bridges and structural rs_mass_MeV formulas agree exactly on within-family ratios for u/c/t quarks. The anchor mass is the native RSBridge expression M0 * exp(((rung f - 8 + gap(ZOf f)) * log phi)), with no SI display divisor. The upstream row_anchor_charm_up_ratio_exp supplies the equivalent exponential form of the same ratio, using the rung difference of 11 for charm and up (which share Z).
proof idea
The term proof first rewrites via the exponential ratio from row_anchor_charm_up_ratio_exp, then invokes Real.rpow_def_of_pos on the positive phi, and finishes with ring_nf algebraic normalization.
why it matters
This result feeds the parent theorem row_charm_up_structural_anchor_agree, which equates the structural charm/up ratio to the anchor ratio. It completes a P0-Q bridge row in the physical derivation plan, confirming that within-family ratios match under the phi-ladder mass formula (yardstick * phi^(rung-8+gap(Z))) and the eight-tick octave. The absolute MeV calibration to PDG values remains a partial theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.