ckm_hierarchy_one_statement
plain-language theorem explainer
The theorem asserts that the six Standard Model quarks occupy rungs 8,9,14,17,22,30 on the phi-ladder, obey strict mass ordering, advance by exact multiplicative factor phi at each rung, and yield a top-to-up ratio above 30000. Particle physicists constructing fermion hierarchies inside Recognition Science would cite this structural result for the CKM sector. The proof is a one-line term that assembles reflexivity on the count, the rung-ordering lemma, the geometric mass lemma, and the explicit ratio bound.
Claim. The Standard Model contains exactly six quarks whose rung numbers satisfy the strict chain $r_u < r_d < r_s < r_c < r_b < r_t$, the mass at rung $k+1$ equals the mass at rung $k$ multiplied by the golden ratio for any base unit, and the top-to-up mass ratio exceeds 30000.
background
Recognition Science places quark masses on the phi-ladder via the definition mass_at_rung m_unit k := m_unit * phi^k. The module assigns the six canonical rungs from the SU(3)×SU(2)×U(1) gauge structure on the third generation: up at 8, down at 9, strange at 14, charm at 17, bottom at 22, top at 30. Upstream results supply the integer rung label for each fermion class and the multiplicative step encoded in mass_geometric.
proof idea
The proof is a term-mode construction that packages four components: reflexivity establishes the quark count equals six, the lemma quark_rungs_strict_ordering supplies the chain of rung inequalities, mass_geometric delivers the universal per-rung multiplication by phi, and mass_ratio_top_up_above_30000 provides the concrete lower bound on the top-to-up ratio.
why it matters
This theorem consolidates the phi-ladder account of the CKM hierarchy and closes Track F7 by exhibiting the exact six-quark spectrum together with the geometric progression. It instantiates the self-similar fixed point phi from the forcing chain and the mass formula on the ladder. The result supplies the structural prediction that the top-to-up ratio equals phi^22 approximately 39089, within a factor of two of the empirical value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.