mass_ratio_top_up_above_30000
plain-language theorem explainer
The theorem establishes a numerical lower bound showing that the top-to-up quark mass ratio on the phi-ladder exceeds 30,000. Researchers modeling Standard Model hierarchies via self-similar scaling would cite this to confirm the phi^22 prediction sits within a factor of three of the observed 80,000 ratio. The proof proceeds by invoking a lower bound on phi and verifying the power inequality through explicit multiplication and comparison.
Claim. $30000 < m_t / m_u$ where the ratio equals $phi^{22}$ and $phi$ is the golden ratio fixed point of the recognition geometry.
background
The module derives the six-quark CKM mass hierarchy from the phi-ladder in Recognition Science. Quark masses sit at integer rungs with $m_quark(k) = m_unit · phi^k$ and $m_unit = phi^{-5}/8$. The assignments are u at rung 8 and t at rung 30, so the top-to-up ratio is exactly $phi^{22}$. The definition mass_ratio_top_up unfolds directly to this power. An upstream lemma supplies the concrete lower bound $1.61 < phi$.
proof idea
The tactic proof unfolds mass_ratio_top_up to $phi^{22}$. It applies the lemma phi_gt_onePointSixOne to obtain $1.61 < phi$. Separate subgoals establish $(1.61)^{11} > 175$ by ring expansion and norm_num, then square both sides to exceed 30625. The final linarith step closes the comparison after rewriting the square.
why it matters
This bound populates the master certificate CKMHierarchyFromPhiLadderCert and the one-statement theorem ckm_hierarchy_one_statement. It supplies the concrete numerical anchor for Track F7, confirming that the structural $phi^{22}$ prediction remains consistent with empirical ratios. The result rests on the phi fixed point (T6) and eight-tick octave (T7) from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.