Explicit Iterate Formula

After k steps of the Collatz function, the result satisfies 2^a · T^k(n) = 3^b · n + c where a counts even steps, b counts odd steps, and c is an accumulator. This is the algebraic identity underlying all cycle analysis.

theorem Collatz.iterate_linear_form (n k : ℕ) : ∃ (a : ℕ) (b : ℕ) (c : ℕ), a + b = k ∧ 2 ^ a * collatz^[k] n = 3 ^ b * n + c