Section 1: Inductive Definition

inductive Collatz.CollatzTree : ℕ → Prop

Membership in the Collatz preimage tree rooted at 1. Built by iterating preimage operations backward from 1: every n has even preimage 2n, and odd preimage (n-1)/3 precisely when n ≡ 4 (mod 6).

• base : CollatzTree 1
• even_child {n : ℕ} : CollatzTree n → CollatzTree (2 * n)
• odd_child {n : ℕ} : CollatzTree n → n % 6 = 4 → CollatzTree ((n - 1) / 3)

Section 2: Basic Members

theorem Collatz.collatzTree_two : CollatzTree 2

theorem Collatz.collatzTree_four : CollatzTree 4

Section 3: Tree → Converges

theorem Collatz.CollatzTree.converges {n : ℕ} : CollatzTree n → CollatzConverges n

Section 4: Backward Closure

theorem Collatz.collatzTree_of_collatz {n : ℕ} (h : CollatzTree (collatz n)) : CollatzTree n

If collatz n is in the tree, then n is in the tree. This is the key lemma: it lets us "pull back" tree membership through any single Collatz step.

Section 5: Converges → Tree

theorem Collatz.CollatzConverges.collatzTree {n : ℕ} (h : CollatzConverges n) : CollatzTree n

Section 6: Equivalence

theorem Collatz.collatzTree_iff_converges {n : ℕ} : CollatzTree n ↔ CollatzConverges n

Section 7: Conjecture Reformulation

theorem Collatz.collatz_conjecture_iff_tree : (∀ (n : ℕ), 1 ≤ n → CollatzConverges n) ↔ ∀ (n : ℕ), 1 ≤ n → CollatzTree n

theorem Collatz.collatz_conjecture_tree (n : ℕ) : 1 ≤ n → CollatzTree n

The Collatz conjecture, reformulated: every positive integer belongs to the preimage tree rooted at 1.

Section 8: Tree Structure Properties

theorem Collatz.not_collatzTree_zero : ¬CollatzTree 0

theorem Collatz.CollatzTree.pos {n : ℕ} (h : CollatzTree n) : 0 < n

theorem Collatz.CollatzTree.collatz {n : ℕ} (h : CollatzTree n) : CollatzTree (Collatz.collatz n)