up_rung
plain-language theorem explainer
The up-quark rung is assigned the integer 8 as the base position for the lightest up-type quark on the phi-ladder. CKM hierarchy modelers cite this constant when deriving mass ratios such as phi^22 for the top-to-up ratio from the Recognition Science geometry. The definition is a direct constant assignment with no computation or hypotheses.
Claim. The up-quark rung number equals the natural number 8.
background
In the CKM Quark Mass Hierarchy from φ-Ladder module, quark masses sit on the φ-ladder via m_quark(k) = m_unit · φ^k with m_unit = φ^{-5}/8. The module documentation assigns the six canonical rungs from the SU(3)×SU(2)×U(1) gauge structure on Q3: up at 8, down at 9, strange at 14, charm at 17, bottom at 22, top at 30. Upstream rung definitions in anchor policies and constants supply integer positions for sectors including up-quarks.
proof idea
The definition is a direct constant assignment of 8. No lemmas or tactics are applied.
why it matters
This definition supplies the base rung for the up quark inside the CKMHierarchyFromPhiLadderCert structure and the one-statement theorem ckm_hierarchy_one_statement. It fills Track F7 by enabling the structural prediction m_t / m_u = φ^22 within a factor of 2 of the empirical ratio, consistent with the phi-ladder forced by recognition geometry and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.