mass_strict_increasing
plain-language theorem explainer
Mass at rung k is strictly smaller than mass at rung m whenever k < m and the base unit is positive. Quark mass modelers cite this to lock in the ordering u < d < s < c < b < t on the phi-ladder. The term proof unfolds the mass definition, pulls 1 < phi from one_lt_phi, applies the power monotonicity lemma, and finishes with left-multiplication by the positive scalar.
Claim. Let $m_0 > 0$ be a positive real. For natural numbers $k < m$, $m_0 phi^k < m_0 phi^m$, where the mass function at rung $k$ is defined by $m_0 cdot phi^k$.
background
The module constructs the CKM quark mass hierarchy directly from the phi-ladder. Mass at rung k is the definition mass_at_rung m_unit k := m_unit * phi ^ k. The six quark rungs run from up_rung = 8 to top_rung = 30, with the mass formula m_quark(k) = m_unit * phi^k and m_unit = phi^(-5)/8 drawn from the recognition geometry. Upstream, one_lt_phi supplies the key fact 1 < phi, proved in Constants by comparing the golden-ratio expression to 1 via square-root inequalities.
proof idea
Term proof. Unfold mass_at_rung to expose the product m_unit * phi^k. Obtain 1 < phi via one_lt_phi. Apply pow_lt_pow_right₀ to the exponent inequality k < m and base phi > 1. Finish with mul_lt_mul_of_pos_left using the hypothesis 0 < m_unit.
why it matters
Supplies the strict monotonicity clause inside the CKMHierarchyFromPhiLadderCert structure, which assembles the full Track F7 certificate. The certificate encodes the six-quark ordering, geometric mass steps, and the top-to-up ratio phi^22. It closes the mass-ordering step required for the master certificate that derives all quark ratios from Constants.phi alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.