rung_sdgt_down
plain-language theorem explainer
The definition supplies a lookup table for SDGT rungs of down quarks, mapping d to 4, s to 10 and b to 18. Mass modelers in the Recognition Science framework cite this table when fixing the exponent on the phi ladder for down-type fermions. The implementation is a direct pattern match on the input string that returns the listed integers or zero.
Claim. The SDGT down-quark rung map $r_↓^{SDGT}(name)$ satisfies $r_↓^{SDGT}(``d'')=4$, $r_↓^{SDGT}(``s'')=10$, $r_↓^{SDGT}(``b'')=18$, and equals 0 for every other string $name$.
background
Rung values fix the power of phi in the mass formula yardstick times phi to the power of rung minus 8 plus the gap term. The AnchorPolicy module supplies a sector dispatcher that routes to integer tables for leptons, up quarks, down quarks or electroweak bosons. This definition specializes the down-quark case under the SDGT policy while the composite selector leaves leptons and bosons unchanged.
proof idea
The definition is realized by a match expression on the name string. It returns the constant 4 for d, 10 for s, 18 for b, and 0 otherwise. No lemmas are invoked.
why it matters
The table is called by the SDGT rung selector in the same module, which supports downstream mass prediction. It encodes the SDGT adjustment to the down-sector rungs on the phi ladder, consistent with the eight-tick octave in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.