top_rung
plain-language theorem explainer
The definition assigns the natural number 30 to the top-quark rung on the phi-ladder. Researchers deriving CKM mass hierarchies from recognition geometry cite this as the scale-saturating position for the heaviest third-generation up-type quark. It is a direct constant assignment with no computation or lemma application.
Claim. The top-quark rung on the phi-ladder is the natural number 30.
background
In the Recognition Science framework the phi-ladder places quark masses at integer rungs via the relation m_quark(k) = m_unit · phi^k with m_unit = phi^{-5}/8. The module documentation fixes the six canonical rungs as u at 8, d at 9, s at 14, c at 17, b at 22 and t at 30 to reproduce the observed five-order-of-magnitude hierarchy and the structural ratio m_t/m_u = phi^{22}.
proof idea
Direct constant definition assigning the value 30 to top_rung. No lemmas, tactics or upstream results are invoked beyond the constant declaration itself.
why it matters
This supplies the top-rung index required by the master certificate CKMHierarchyFromPhiLadderCert and the one-statement theorem ckm_hierarchy_one_statement. It completes the phi-ladder assignment that yields the prediction phi^{22} > 39000, within a factor of two of the empirical top-to-up ratio, and feeds the strict-ordering theorem quark_rungs_strict_ordering together with mass_strict_increasing. It addresses the Standard Model's lack of explanation for the quark mass hierarchy by realizing the scale-saturating rung forced by the gauge structure on Q3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.