r_down
plain-language theorem explainer
The down-type quark rung assignment supplies integer positions on the phi-ladder for the d, s, and b quarks. Researchers deriving fermion masses cite this to anchor the exponential scaling in the Recognition mass formula. It is implemented as a direct alias to the pattern-matching definition in the Anchor module.
Claim. Define the function $r_↓ : String → ℤ$ by $r_↓(``d'') = 4$, $r_↓(``s'') = 15$, $r_↓(``b'') = 21$, and $r_↓(x) = 0$ for other strings $x$.
background
In the Recognition Science framework, rung integers fix the exponent in the mass formula yardstick × ϕ^(rung − 8 + gap(Z)). The Anchor module introduces sector-specific rung functions, with down-type quarks using base value 4 plus tau increments for higher generations. AnchorPolicy re-exports these as policy aliases for use in baseline derivations and verification theorems. The upstream definition states: Rung integers for down-type quarks. d: 4, s: 4 + tau(1) = 15, b: 4 + tau(2) = 21.
proof idea
This declaration is a one-line wrapper that aliases the down-quark rung function from the Anchor module.
why it matters
This alias enables the rung selector in AnchorPolicy and supports theorems verifying down-generation spacing and quark baseline matches. It implements the down-sector contribution to the phi-ladder mass predictions, aligning with the eight-tick octave and D=3 spatial dimensions in the forcing chain. Downstream certificates such as QuarkVerificationCert rely on the spacing properties r_down s − r_down d = 11 and r_down b − r_down d = 17.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.