up_charm_to_up_ratio
plain-language theorem explainer
The theorem proves that the Recognition Science mass ratio of the charm quark to the up quark in the up-type sector equals phi to the eleventh power. Researchers checking generational spacing on the phi-ladder against PDG data would cite this when confirming the mass formula for up-type quarks. The proof reduces the ratio by unfolding rs_mass_MeV, simplifying with r_up and the edge-count constants, then applying field_simp and zpow arithmetic on the positive phi.
Claim. Let $m(r)$ denote the Recognition Science mass in MeV for an up-type quark at rung $r$, given by $m(r) = 2^{-1} phi^{-5} phi^{35} phi^r / 10^6 = phi^{30+r}/(2 times 10^6)$. Then $m(15)/m(4) = phi^{11}$, where rung 15 corresponds to the charm quark and rung 4 to the up quark.
background
The module compares RS quark masses to PDG 2024 values under the up-sector formula $m(UpQuark, r) = phi^{30+r}/(2 times 10^6)$ MeV with $B_pow = -1$ and $r0 = 35$. Rung assignments are $r_u = 4$, $r_c = 15$, $r_t = 21$ from Anchor. The ratio isolates the pure phi-power spacing between generations. Upstream constants include phi_pos from Constants, active_edges_per_tick (one edge transition per tick), cube_edges ($D times 2^{D-1}$), passive_field_edges (cube_edges minus active), and wallpaper_groups (17).
proof idea
Term proof begins with simp on r_up, tau, Anchor.E_passive, Anchor.W, passive_field_edges, cube_edges, active_edges_per_tick, D and wallpaper_groups. It unfolds rs_mass_MeV then repeats simp with B_pow, r0, A. After introducing phi_pos and its nonzero property, field_simp cancels denominators; rw with zpow_natCast and zpow_add_0 reduces the exponent difference to 11, closed by congr.
why it matters
The result verifies self-similar spacing on the phi-ladder for up-type quarks, consistent with T6 (phi as self-similar fixed point) and the mass formula derived from the Recognition Composition Law under D=3. It closes a verification step in the quark sector against PDG data even though no downstream theorem yet references it. The parent structure is the mass anchor in Anchor together with the forcing chain constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.