CKMHierarchyFromPhiLadderCert
plain-language theorem explainer
The CKMHierarchyFromPhiLadderCert structure collects eight arithmetic properties of the six-quark mass hierarchy on the phi-ladder. Particle physicists working on fermion mass patterns would cite it to obtain the top-to-up ratio as phi^22 from rung assignments. The definition assembles prior rung constants and the geometric mass theorem by direct packaging with no internal proof steps.
Claim. The certificate asserts exactly six quarks whose rungs satisfy $8 < 9 < 14 < 17 < 22 < 30$, masses obey $m(k+1) = m(k) · φ$ for any positive base unit, the top-to-up ratio $φ^{22}$ is positive and exceeds 30000, the up-quark sits at rung 8 and the top-quark at rung 30.
background
In Recognition Science the phi-ladder places quark masses at integer rungs via $m(k) = m_{unit} · φ^k$. The module fixes the six rungs from gauge structure on $Q_3$: up at 8, down at 9, strange at 14, charm at 17, bottom at 22, top at 30. The upstream mass_at_rung definition is $m_{unit} · φ^k$; the mass_geometric theorem states adjacent rungs differ by exactly $φ$, proved by unfolding and applying pow_succ together with ring. The mass_ratio_top_up is defined directly as $φ^{22}$.
proof idea
The structure is a direct definition that packages the rung equalities, the strict ordering, the geometric progression from mass_geometric, and the positivity bound on $φ^{22}$. No tactics appear inside the structure; the downstream inhabiting term supplies concrete values by reflexivity on the rung constants and prior lemmas.
why it matters
This certificate closes Track F7 by packaging the structural prediction $m_t / m_u = φ^{22} ≈ 39089$. It is used by ckmHierarchyFromPhiLadderCert to witness the master certificate. The result follows the phi fixed point in the forcing chain and supports the mass formula on the phi-ladder; the factor-of-two gap with the empirical ratio is recorded as a gap-45 scale-running correction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.