Section 1: Even Preimage

theorem Collatz.collatz_double (n : ℕ) : collatz (2 * n) = n

theorem Collatz.collatz_preimage_of_even {m n : ℕ} (hm : m % 2 = 0) (h : collatz m = n) : m = 2 * n

Section 2: Odd Preimage Existence

theorem Collatz.odd_preimage_is_odd {n : ℕ} (h : n % 6 = 4) : (n - 1) / 3 % 2 = 1

theorem Collatz.odd_preimage_val {n : ℕ} (h : n % 6 = 4) : collatz ((n - 1) / 3) = n

theorem Collatz.no_odd_preimage {n : ℕ} (h : n % 6 ≠ 4) {m : ℕ} (hm : m % 2 = 1) : collatz m ≠ n

theorem Collatz.collatz_preimage_of_odd {m n : ℕ} (hm : m % 2 = 1) (h : collatz m = n) : m = (n - 1) / 3

Section 3: Preimage Properties

theorem Collatz.odd_preimage_lt {n : ℕ} (h : n % 6 = 4) : (n - 1) / 3 < n

theorem Collatz.preimage_even_ne_odd {n : ℕ} (h : n % 6 = 4) : (n - 1) / 3 ≠ 2 * n

Section 4: Injectivity

theorem Collatz.collatz_injective_on_odd {m₁ m₂ : ℕ} (h₁ : m₁ % 2 = 1) (h₂ : m₂ % 2 = 1) (h : collatz m₁ = collatz m₂) : m₁ = m₂

theorem Collatz.collatz_injective_on_even {m₁ m₂ : ℕ} (h₁ : m₁ % 2 = 0) (h₂ : m₂ % 2 = 0) (h : collatz m₁ = collatz m₂) : m₁ = m₂

Section 5: Convergence Propagation (Backward)

theorem Collatz.converges_double {n : ℕ} (h : CollatzConverges n) : CollatzConverges (2 * n)

theorem Collatz.converges_odd_preimage {n : ℕ} (h : CollatzConverges n) (hmod : n % 6 = 4) : CollatzConverges ((n - 1) / 3)