ckmHierarchyFromPhiLadderCert
plain-language theorem explainer
The declaration constructs the master certificate asserting the six-quark CKM hierarchy on the phi-ladder with rungs 8,9,14,17,22,30. Researchers deriving closed-form fermion mass ratios in Recognition Science cite it for the structural claim that top-to-up ratio equals phi^22. Construction is a direct record that supplies reflexivity on equalities and references the geometric mass theorem plus strict ordering lemma.
Claim. The certificate asserts six quarks with rungs satisfying $8<9<14<17<22<30$, adjacent masses obeying $m(k+1)=m(k)·φ$ for any unit mass $m$, and the top-to-up ratio exactly $φ^{22}$.
background
The module establishes the phi-ladder for quark masses inside Recognition Science, where each rung multiplies mass by the golden ratio φ derived from the J-cost fixed point. The unit mass is $E_{coh}/8=φ^{-5}/8$. Quark rungs are fixed by gauge structure on the third generation: up at 8, down at 9, strange at 14, charm at 17, bottom at 22, top at 30. The upstream mass_geometric theorem states that mass_at_rung m_unit (k+1) equals mass_at_rung m_unit k times phi, proved by unfolding the power definition and applying ring arithmetic.
proof idea
The definition builds the CKMHierarchyFromPhiLadderCert structure by direct field assignment. quark_count_eq and the rung equalities use reflexivity. quark_rungs_strict_ordering and mass_strict_increasing reference the corresponding in-module lemmas. mass_geometric applies the upstream theorem that adjacent rungs differ by exactly phi. The two top-up ratio fields invoke the positivity and bound lemmas already proved in the same file.
why it matters
This definition inhabits the master certificate for Track F7, supplying the closed structural account of the six-quark mass hierarchy. It completes the one-statement summary that m_t/m_u = φ^22 ≈ 39089, within factor two of the observed 80000. The result rests on the phi-ladder forced by the recognition composition law and the eight-tick octave; it closes the gap between the J-uniqueness fixed point and observable fermion scales without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.