mass_ratio_top_up_pos
plain-language theorem explainer
The theorem establishes strict positivity of the top-to-up quark mass ratio defined as φ raised to the power 22. Researchers assembling Recognition Science predictions for the six-quark hierarchy cite this when completing the master certificate for CKM structure. The argument is a one-line term-mode reduction that unfolds the ratio definition and applies the positivity of real powers for positive base.
Claim. The top-to-up quark mass ratio satisfies $0 < phi^{22}$, where the exponent 22 equals the difference between the top rung (30) and up rung (8) on the φ-ladder.
background
In the CKMHierarchyFromPhiLadder module, the six quarks occupy fixed rungs on the φ-ladder forced by the gauge structure on Q₃: up at rung 8, down at 9, strange at 14, charm at 17, bottom at 22, and top at 30. The mass at rung k is m_unit · φ^k with m_unit = φ^{-5}/8, so the top-to-up ratio is exactly φ^{22}. The module documentation records this structural prediction and notes that φ^{22} ≈ 39089 lies within a factor of two of the empirical ratio near 80000.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition mass_ratio_top_up := phi ^ 22 and applies the lemma pow_pos to the positivity of phi.
why it matters
This positivity clause is required by the master certificate CKMHierarchyFromPhiLadderCert, which collects eight clauses on quark count, strict rung ordering, and geometric mass progression. It completes the structural claim of Track F7 that m_t / m_u = φ^{22}. The result feeds the downstream band theorem and the full certificate structure; the remaining numerical offset from measured masses remains an open calibration question within the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.