down_rung
plain-language theorem explainer
Recognition Science assigns the down quark to rung 9 on the phi-ladder, one step above the up quark at rung 8. Modelers of quark mass hierarchies cite this constant when stating the six-quark ordering and geometric ratios. The assignment is a direct constant definition that supplies the value required by the hierarchy certificate and ordering theorem.
Claim. The rung number for the down quark is the integer $9$.
background
In the CKM Quark Mass Hierarchy from phi-Ladder module, quark masses occupy discrete positions on the phi-ladder with mass proportional to phi to the rung power. The module lists the canonical assignments: up at rung 8, down at rung 9, strange at 14, charm at 17, bottom at 22, and top at 30. These positions are forced by the SU(3) times SU(2) times U(1) gauge structure on the third-generation quark doublet. Upstream rung definitions in Constants, AnchorPolicy, and RSBridge.Anchor supply the general integer-valued rung map for fermions and sectors, which this module specializes to the six quarks.
proof idea
One-line definition that directly sets the constant to the natural number 9.
why it matters
The definition supplies the down_rung value required by CKMHierarchyFromPhiLadderCert and the one-statement theorem ckm_hierarchy_one_statement. It completes the rung list that yields the structural claim m_t over m_u equals phi to the 22, within a factor of two of the observed ratio. The assignment participates in the phi-ladder construction that follows from the T5 J-uniqueness and T6 self-similar fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.