Mod 4 Two-Step Behavior

When n % 4 is known, the result of two consecutive Collatz steps is fully determined. This is because n mod 4 encodes the parity of both n and the result of the first step.

theorem Collatz.collatz_collatz_mod4_0 {n : ℕ} (h : n % 4 = 0) : collatz (collatz n) = n / 4

theorem Collatz.collatz_collatz_mod4_1 {n : ℕ} (h : n % 4 = 1) : collatz (collatz n) = (3 * n + 1) / 2

theorem Collatz.collatz_collatz_mod4_2 {n : ℕ} (h : n % 4 = 2) : collatz (collatz n) = 3 * (n / 2) + 1

theorem Collatz.collatz_collatz_mod4_3 {n : ℕ} (h : n % 4 = 3) : collatz (collatz n) = (3 * n + 1) / 2

Descent

theorem Collatz.collatz_collatz_lt_of_mod4_0 {n : ℕ} (hn : 0 < n) (h : n % 4 = 0) : collatz (collatz n) < n

Parity of Shortcut Output

These determine whether the third Collatz step is a halving or an odd step.

theorem Collatz.shortcut_even_of_mod4_1 {n : ℕ} (h : n % 4 = 1) : collatzShortcut n % 2 = 0

theorem Collatz.shortcut_odd_of_mod4_3 {n : ℕ} (h : n % 4 = 3) : collatzShortcut n % 2 = 1

Three-Step Closed Form

theorem Collatz.three_step_mod4_1 {n : ℕ} (h : n % 4 = 1) : collatz (collatz (collatz n)) = (3 * n + 1) / 4