row_structural_charm_up_ratio_rpow
plain-language theorem explainer
The theorem establishes that the ratio of predicted structural masses for the charm and up quarks equals phi raised to the eleventh power with a real exponent. Researchers deriving quark mass ladders within the Recognition Science framework cite this when confirming power-law consistency on within-family ratios. The proof is a one-line wrapper that lifts the natural-number ratio theorem to the real case via exponent casting.
Claim. $m_c / m_u = phi^{11}$ where $m_c$ and $m_u$ are the structural mass predictions for the charm quark (rung 15) and up quark (rung 4) on the phi-ladder.
background
The Quark Absolute Bridge Score Card module deepens the existing QuarkScoreCard by proving exact agreement on within-family ratios for the u/c/t sector. Structural predictions are defined via the phi-ladder: up-quark mass equals phi to the 34 divided by 2 million, charm-quark mass equals phi to the 45 divided by 2 million. This rests on the prior row_charm_up_ratio theorem, which already establishes the same ratio as phi to the 11 using natural-number exponentiation.
proof idea
The proof is a one-line wrapper that applies the row_charm_up_ratio theorem after rewriting the exponent via Real.rpow_natCast.
why it matters
This declaration feeds the row_charm_up_structural_anchor_agree theorem, which equates the structural ratio to the corresponding massAtAnchor ratio. It completes the P0-Q bridge row for the charm/up structural ratio expressed as a real-power phi law, supporting consistency between rung-based predictions and continuous expressions. It touches the open absolute MeV bridge for quarks, where the rs_mass_MeV yardstick and native anchor formula must still be shown to calibrate to the same quantity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.