Collatz conjecture

Collatz Conjecture (3n+1 Problem): Starting from any positive integer $n$, the iteration $f(n) = n/2$ (if $n$ even) or $f(n) = 3n+1$ (if $n$ odd) eventually reaches 1.

Example: $6 \to 3 \to 10 \to 5 \to 16 \to 8 \to 4 \to 2 \to 1$.

Proposed by Lothar Collatz in 1937. Verified for all integers up to $2^{68}$. Tao (2019) proved almost all orbits reach arbitrarily small values. Erdős said 'Mathematics is not yet ready for such problems'.

Formalization Note The Collatz step is imported from the reusable collatzStepMap definition module so that proof submissions can be checked.