mass_ratio_top_up_pos_band
plain-language theorem explainer
The theorem asserts that the top-to-up quark mass ratio on the phi-ladder is strictly positive. Researchers deriving the six-quark spectrum or CKM hierarchy from recognition geometry would cite it as one clause in the structural master certificate. The proof is a direct one-line application of the underlying positivity lemma for the same ratio.
Claim. $0 < m_t / m_u$, where $m_t$ and $m_u$ are the top and up quark masses placed at rungs 30 and 8 on the phi-ladder with unit mass $m_{unit} = E_{coh}/8$.
background
The module derives the CKM quark mass hierarchy from the phi-ladder forced by recognition geometry. Quark masses occupy discrete rungs: $m(k) = m_{unit} · phi^k$, with $m_{unit} = phi^{-5}/8$. The six quarks sit at rungs 8 (u), 9 (d), 14 (s), 17 (c), 22 (b), and 30 (t). Adjacent rungs differ by exactly phi by the mass-geometric lemma. The local setting is the eight-clause master certificate that closes the structural derivation of the observed hierarchy without axioms or sorries.
proof idea
This is a one-line wrapper that applies the positivity lemma mass_ratio_top_up_pos. No further tactics or reductions are used.
why it matters
It supplies clause 5 of the eight-clause master certificate for the CKM hierarchy (Track F7). The certificate lists six-quark structure, strict rung ordering, geometric mass steps, monotonicity, this positivity result, the numerical bound near 39089, and the explicit rung assignments for u and t. The result anchors the prediction $m_t/m_u = phi^{22}$ and sits inside the broader forcing chain that fixes phi as the self-similar point and yields D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.