No Nontrivial Small Cycles

If n converges to 1, the only cycle n can be on is {1, 2, 4}. Combined with computational verification that all n ≤ 20 converge, we rule out nontrivial cycles for small values.

The orbit of 1 is {1, 4, 2}

theorem Collatz.collatz_iterate_one (m : ℕ) : collatz^[m] 1 = 1 ∨ collatz^[m] 1 = 4 ∨ collatz^[m] 1 = 2

Every iterate of 1 under collatz is in {1, 4, 2}. Uses the 3-periodicity of 1.

Periodic + convergent implies trivial cycle

theorem Collatz.periodic_of_converges {n p : ℕ} (hp : 0 < p) (hcyc : collatz^[p] n = n) (hconv : CollatzConverges n) : n = 1 ∨ n = 2 ∨ n = 4

If n is both periodic and convergent, then n ∈ {1, 2, 4}.

No nontrivial cycles for n ≤ 20

theorem Collatz.no_nontrivial_cycle_le_twenty {n p : ℕ} (hp : 0 < p) (hn1 : 1 ≤ n) (hn2 : n ≤ 20) (hcyc : collatz^[p] n = n) : n = 1 ∨ n = 2 ∨ n = 4

No nontrivial cycle exists among values 1 through 20.