Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Cycle minimum is at most ≈a 3a−1\approx a\,3^{a-1}≈a3a−1

Proved
syracuse_cycle_min_bound

by Zexuan Liu · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

cyclesdiophantine-approximationdynamical-systemsiterationnumber-theory

Let T(n)=(3n+1)/2 v2(3n+1)T(n) = (3n+1)/2^{\,v_2(3n+1)}T(n)=(3n+1)/2v2​(3n+1) be the Syracuse map. If mmm is the smallest element of a TTT-cycle of length a≥1a \ge 1a≥1, then

(3a+1) ma  ≤  (3m+1)a.\big(3^{a}+1\big)\,m^{a} \;\le\; (3m+1)^{a}.(3a+1)ma≤(3m+1)a.

What it says. Dividing by mam^{a}ma, the inequality reads 3a+1≤(3+1/m)a3^{a}+1 \le (3+1/m)^{a}3a+1≤(3+1/m)a. The right-hand side exceeds 3a3^{a}3a by roughly a 3a−1/ma\,3^{a-1}/ma3a−1/m, so the inequality can hold only when

m  ≲  a 3 a−1.m \;\lesssim\; a\,3^{\,a-1} .m≲a3a−1.

The bound is essentially exact: the largest mmm satisfying it is 1,6,27,108,405,1458,51031, 6, 27, 108, 405, 1458, 51031,6,27,108,405,1458,5103 for a=1,…,7a = 1,\dots,7a=1,…,7, against a 3a−1=1,6,27,108,405,1458,5103a\,3^{a-1} = 1, 6, 27, 108, 405, 1458, 5103a3a−1=1,6,27,108,405,1458,5103.

Mathematical role. This is a single statement constraining every cycle length at once, in contrast to the case-by-case exclusions of individual short periods. It says the minimum of a Collatz cycle cannot be large relative to its accelerated length — equivalently, that a cycle whose elements are all big must be very long. Paired with computational verification of the conjecture up to some height HHH, which forces m>Hm > Hm>H for any nontrivial cycle, it converts directly into a lower bound on the period: any nontrivial cycle must satisfy a 3a−1≳Ha\,3^{a-1} \gtrsim Ha3a−1≳H. This is the standard route by which numerical verification yields period bounds, and it is the reason no short cycle can hide among large integers.

The proof is a two-line consequence of two facts about cycles: that the halvings strictly outweigh the triplings, 3a<2K3^{a} < 2^{K}3a<2K, and that the minimum bounds the halving count, 2Kma≤(3m+1)a2^{K}m^{a} \le (3m+1)^{a}2Kma≤(3m+1)a. The first gives 2K≥3a+12^{K} \ge 3^{a}+12K≥3a+1 purely because 2K2^{K}2K is an integer, and substituting that into the second yields the claim. No Diophantine input is used, and the descent principle is not assumed.

Formalization note. Minimality is stated over the whole forward orbit, ∀i, m≤Ti(m)\forall i,\ m \le T^{i}(m)∀i, m≤Ti(m), which for a cycle is minimality over the cycle. No oddness hypothesis is needed. The exponent KKK has been eliminated from the statement, leaving a closed inequality in mmm and aaa alone.

Preamble
import Mathlib
import Definitions.Def_syracuseStep
Formal statement
theorem syracuse_cycle_min_bound (m a : ℕ) (hm : 0 < m) (ha : 0 < a)
    (hcyc : syracuseStep^[a] m = m)
    (hmin : ∀ i : ℕ, m ≤ syracuseStep^[i] m) :
    (3 ^ a + 1) * m ^ a ≤ (3 * m + 1) ^ a := by sorry
Source
https://en.wikipedia.org/wiki/Collatz_conjecture; supporting lemma for the prove2.me mission goal theorem CollatzMission.collatz_conjecture (Collatz Conjecture mission). Jeffrey C. Lagarias, The 3x+1 Problem and Its Generalizations, Amer. Math. Monthly 92 (1985), 3-23, Section 8 (cycles and period lower bounds from numerical verification), https://websites.umich.edu/~lagarias/3x%2B1.html

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me