top_to_up_ratio
plain-language theorem explainer
The theorem shows that the RS up-sector mass ratio of the top quark to the up quark equals phi to the 17th power. Quark-mass modelers comparing phi-ladder predictions to PDG data would cite this when checking exponent differences for rungs 21 and 4. The proof reduces the ratio by unfolding the mass definition, substituting edge constants from AlphaDerivation, and simplifying the resulting phi exponents via field_simp and zpow arithmetic.
Claim. In the up-quark sector the ratio of the top-quark mass to the up-quark mass satisfies $m_t / m_u = phi^{17}$, where each mass is given by $phi^{30+r}/(2 times 10^6)$ MeV with rung integers $r_t=21$ and $r_u=4$.
background
The QuarkVerification module supplies machine-checked comparisons of RS mass predictions against PDG values while treating experimental numbers as imported constants. For the up sector (B_pow = -1, r0 = 35) the mass formula simplifies to $m(UpQuark,r) = phi^{30+r}/(2 times 10^6)$ MeV. The rungs are fixed by Anchor: u at r=4, c at r=15, t at r=21. Upstream constants include phi from Constants, D=3, and the edge counts active_edges_per_tick=1, cube_edges=D*2^{D-1}, passive_field_edges=11, and wallpaper_groups=17 from AlphaDerivation.
proof idea
The term proof first applies simp to replace r_up, tau, Anchor.E_passive, Anchor.W and the AlphaDerivation edge definitions. It unfolds rs_mass_MeV, repeats the simp step, introduces phi positivity, invokes field_simp, rewrites with zpow_natCast and zpow_add_0, and finishes with congr.
why it matters
The result confirms the exact exponent gap of 17 between the t and u rungs inside the up-sector mass formula, completing one verification step for the phi-ladder mass predictions. It sits inside the T5-T6 forcing chain that fixes phi as the self-similar fixed point and supports the D=3 spatial dimension used throughout the framework. No downstream theorems are recorded, yet the declaration contributes to the module's zero-sorry status for quark-sector checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.