r_up_values
plain-language theorem explainer
The declaration fixes the rung parameters for the three up-type quarks in the Recognition Science mass ladder at r_up(u)=4, r_up(c)=15 and r_up(t)=21. A researcher computing predicted quark masses from the phi-ladder would invoke these values to set the generation indices. The proof reduces the statement by unfolding the anchor definitions for r_up and the edge counts, then applies an arithmetic solver.
Claim. $r_ {up}(u)=4$, $r_{up}(c)=15$ and $r_{up}(t)=21$
background
The QuarkVerification module treats PDG values as imported constants while verifying RS-derived rung integers against the mass formulas. For the up sector the formula is m = phi^{30+r} / (2 * 10^6) MeV with r supplied by r_up. Upstream, E_passive is the abbrev passive_field_edges D, cube_edges d := d * 2^{d-1}, active_edges_per_tick := 1, and wallpaper_groups := 17 (Fedorov 1891).
proof idea
The proof is a one-line wrapper that applies simp to unfold r_up, tau, E_passive, W, passive_field_edges, cube_edges, active_edges_per_tick, D and wallpaper_groups, after which omega decides the arithmetic equalities.
why it matters
This theorem supplies the concrete rung values required by upquark_sector_params and the mass formulas in the same module. It closes the specification of the phi-ladder for the up sector, consistent with T5 J-uniqueness and T6 phi fixed point that generate the self-similar scaling. No open questions are addressed; the values are taken as input from the Anchor module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.