Steiner's No 1-Cycle Theorem (Partial)

A "1-cycle" has all odd steps first, then all even steps. We prove the key structural lemmas about consecutive steps and the simplest case: the only 1-cycle with exactly one odd step has n = 1 (the trivial {1,4,2} cycle).

Consecutive odd steps

theorem Collatz.consecutive_odd_steps (n b : ℕ) (hodd : ∀ i < b, collatz^[i] n % 2 = 1) : ∃ (d : ℕ), collatz^[b] n = 3 ^ b * n + d ∧ 2 * d + 1 = 3 ^ b

After b consecutive odd steps starting from n, the value is 3^b * n + d where d = (3^b - 1) / 2, encoded as 2 * d + 1 = 3^b to avoid division.

Consecutive even halvings

theorem Collatz.even_halvings_mul (m j : ℕ) (heven : ∀ i < j, collatz^[i] m % 2 = 0) : collatz^[j] m * 2 ^ j = m

Repeatedly halving an even number: if all intermediate iterates are even, then collatz^[j] m * 2^j = m.

No 1-cycle with b = 1

theorem Collatz.no_one_cycle_b_eq_one {n p : ℕ} (hn : 0 < n) (hp : 2 ≤ p) (hcyc : collatz^[p] n = n) (hodd_first : n % 2 = 1) (heven_rest : ∀ (i : ℕ), 1 ≤ i → i < p → collatz^[i] n % 2 = 0) : n = 1

If n is on a 1-cycle with exactly one odd step (n is odd, then all remaining steps are even), then n = 1. The only such cycle is the trivial {1, 4, 2} cycle.