r_up
plain-language theorem explainer
This definition supplies the integer rung positions on the φ-ladder for up-type quarks u, c, t. Mass derivations in the Recognition framework cite it to fix the base exponents before applying the yardstick scaling. It is realized as a direct pattern match that adds the generation torsion increments 0, 11, 17 to the base value 4.
Claim. The function assigning rung integers to up-type quark labels is defined by $r_{up}(u)=4$, $r_{up}(c)=4+τ(1)=15$, $r_{up}(t)=4+τ(2)=21$, and $r_{up}(x)=0$ otherwise, where $τ$ is the generation torsion map with $τ(1)=11$ and $τ(2)=17$.
background
The Anchor module fixes sector constants from cube geometry in D=3: E_total=12 edges, E_passive=11 passive edges, and W=17 wallpaper groups. Generation torsion τ is the upstream definition τ(0)=0, τ(1)=E_passive, τ(2)=W, supplying the additive offsets for successive generations on the φ-ladder. Rung is the rational type from Support.RungFractions that embeds these integers for the mass formula yardstick · φ^(rung-8+gap(Z)).
proof idea
One-line pattern-matching definition on the String label that returns the literal base 4 for u and delegates the generation increments to the tau function for c and t.
why it matters
It is called by the sector dispatcher rung in AnchorPolicy and by the verification theorems r_up_values and up_generation_spacing that certify the spacings 11 and 17. These values anchor the up-quark sector parameters B_pow=-1, r0=35 inside the QuarkVerificationCert structure. The assignment is consistent with the eight-tick octave and the φ-ladder construction from the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.