r_down
plain-language theorem explainer
r_down maps down-type quark labels to rung integers on the phi-ladder: 4 for d, 15 for s, and 21 for b. Mass derivations cite it to fix the exponent in the yardstick times phi to the power of (rung minus 8 plus gap). The definition is a direct pattern match on the input string that adds the generation torsion tau offsets to the base value 4.
Claim. Define the map from down-type quark labels to integers by $r_↓(d)=4$, $r_↓(s)=4+τ(1)$, $r_↓(b)=4+τ(2)$, and $r_↓(x)=0$ otherwise, where $τ$ is the generation torsion with $τ(1)=11$ and $τ(2)=17$.
background
The module derives all sector constants from D=3 cube geometry: E_total equals 12 edges, E_passive equals 11 passive edges, W equals 17 wallpaper groups, and A equals 1 active edge per tick. These fix the sector yardsticks B_pow and r0 for DownQuark as 23 and -5. The upstream tau definition supplies the generation offsets: τ(0)=0, τ(1)=E_passive=11, τ(2)=W=17. Rung is the abbrev for ℚ that embeds an integer rung into the rational phi-ladder used by the mass formula.
proof idea
The definition is a direct pattern match on the String input. It returns the literal 4 for d, adds tau(1) for s, adds tau(2) for b, and defaults to 0. No lemmas are applied; the body is the case analysis itself.
why it matters
r_down supplies the down-quark rungs consumed by AnchorPolicy.rung and by the down_generation_spacing theorems in QuarkScoreCard and QuarkVerification. It implements the fixed rung integers per species listed in the module doc, which feed the mass formula yardstick * phi^(rung-8+gap(Z)). The declaration closes the structural baseline for down-type fermions inside the D=3 cube-geometry derivation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.