r_up
plain-language theorem explainer
The abbreviation supplies the rung integers for up-type quarks on the Recognition Science mass ladder. Researchers deriving quark masses cite these values to fix the phi-exponent in the mass formula and to verify generation spacings. It is realized as a direct alias to the hardcoded definition in the Anchor module.
Claim. The up-type rung function satisfies $r_ {up} (``u'') = 4$, $r_{up} (``c'') = 15$, $r_{up} (``t'') = 21$ and returns zero for other string inputs.
background
Rung integers set the discrete exponent on the phi-ladder inside the mass formula, which scales as yardstick times phi raised to (rung minus 8 plus gap). The Anchor module fixes the up-type rungs at 4 for the first generation, then 4 plus tau of 1 for charm and 4 plus tau of 2 for top. AnchorPolicy re-exports the definition to support sector selection in the rung dispatcher and downstream mass derivations. The upstream result records rung integers for up-type quarks with u at 4, c at 15 and t at 21.
proof idea
The declaration is a one-line wrapper that aliases the rung integer definition from the Anchor module.
why it matters
It feeds the rung selector used for up-quark cases and appears in verification theorems asserting 11 and 17 spacings between generations. The definition also supports baseline matching theorems and the full verification certificate structure. This supplies the discrete steps on the phi-ladder required by the mass formula, consistent with the self-similar fixed point and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.