Collatz Map Basics

1.2 The Collatz Map

Definition 18
✓
#
Lean declarations:

The Collatz map \(C: \mathbb {N} \to \mathbb {N}\) is defined by

\begin{equation} C(n) = \begin{cases} n/2 & \text{if } n \text{ is even}, \\ 3n + 1 & \text{if } n \text{ is odd}. \end{cases} \end{equation}
9

Lagarias reviewed the history of the map and the conjecture in [ 4 ] .

Definition 19
✓
#

Uses

Lean declarations:

For any \(k \in \mathbb {N}\), the \(k\)-fold iteration of the Collatz map \(C^k: \mathbb {N} \to \mathbb {N}\) is defined recursively by

\begin{equation} C^0(n) = n \end{equation}
12

and

\begin{equation} C^{k+1}(n) = C^k(C(n)). \end{equation}
13

Lemma 20
✓
#

Uses

Lean declarations:

For all \(k, n \in \mathbb {N}\), we have \(C^{k+1}(n) = C(C^k(n))\).

Proof ▶

We proceed by induction on \(k \in \mathbb {N}\). For the base case \(k=0\), \(C^1(n) = C(C^0(n)) = C(n)\) by definition. For the inductive step \(k+1\), we have:

\begin{align*} C^{k+2}(n) & = C^{k+1}(C(n)) \tag {by definition} \\ & = C(C^k(C(n))) \tag {by induction hypothesis applied to $C(n)$} \\ & = C(C^{k+1}(n)) \tag {by definition.} \end{align*}
Lemma 21
✓
#

Uses

Lean declarations:

\(C(0) = 0\).

Proof ▶

Trivial by definition.

Lemma 22
✓
#

Uses

Lean declarations:

For all \(k \in \mathbb {N}\), \(C^k(0) = 0\).

Proof ▶

By induction on \(k\).

Lemma 23
✓
#

Uses

Lean declarations:

If \(n \ge 1\), then \(C(n) \ge 1\).

Proof ▶

If \(n\) is even, then \(n \ge 2\), so \(n/2 \ge 1\). If \(n\) is odd, then \(3n+1 \ge 4 \ge 1\).

Lemma 24
✓
#

Uses

Lean declarations:

If \(n \ge 1\), then for all \(k \in \mathbb {N}\), \(C^k(n) \ge 1\).

Proof ▶

By induction on \(k\), using Lemma 23.

Lemma 25
✓
#

Uses

Lean declarations:

For all \(k \ge 1\), \(C(2^k) = 2^{k-1}\).

Proof ▶

Since \(2^k\) is even for \(k \ge 1\), \(C(2^k) = 2^k/2 = 2^{k-1}\).

Lemma 26
✓
#

Uses

Lean declarations:

For any \(k, m \in \mathbb {N}\), \(C^k(2^k \cdot m) = m\).

Proof ▶

We proceed by induction on \(k \in \mathbb {N}\). The base case \(k=0\) is trivial as \(C^0(m) = m\). For the inductive step \(k+1\), we have

\begin{align*} C^{k+1}(2^{k+1} \cdot m) & = C^k(C(2 \cdot 2^k \cdot m)) \\ & = C^k(2^k \cdot m) \tag {since $2 \cdot 2^k \cdot m$ is even} \\ & = m \tag {by induction hypothesis.} \end{align*}
Lemma 27
✓
#

Uses

Lean declarations:

For all \(l \in \mathbb {N}\), \(C^l(2^l) = 1\).

Proof ▶

By induction on \(l\), using Lemma 25.

Lemma 28
✓
#

Uses

Lean declarations:

For all \(k {\lt} l\), \(C^k(2^l) \neq 1\).

Proof ▶

By induction on \(k\), using Lemma 25.

Lemma 29
✓
#

Uses

Lean declarations:

For all \(l \in \mathbb {N}\), there exists \(n \in \mathbb {N}\) such that \(C^l(n) = 1\) and for all \(k {\lt} l\), \(C^k(n) \neq 1\).

Proof ▶

Choose \(n = 2^l\) and apply Lemmas 27 and 28.

Lemma 30
✓
#

Uses

Lean declarations:

For all \(a, b, n \in \mathbb {N}\), \(C^{a+b}(n) = C^a(C^b(n))\).

Proof ▶

By induction on \(b\).

Lemma 31
✓
#

Uses

Lean declarations:

If \(C^k(n) = n\), then for all \(m \in \mathbb {N}\), \(C^{m \cdot k}(n) = n\).

Proof ▶

By induction on \(m\), using Lemma 30.

Lemma 32
✓
#

Uses

Lean declarations:

If \(n \in \{ 1, 2, 4\} \), then for all \(i \in \mathbb {N}\), \(C^i(n) \in \{ 1, 2, 4\} \).

Proof ▶

By induction on \(i\), checking the cases \(n=1, 2, 4\) for \(C(n)\).

Lemma 33
✓
#

Uses

Lean declarations:

For all \(i \in \mathbb {N}\), \(C^i(1) \le 4\).

Proof ▶

Since \(1 \in \{ 1, 2, 4\} \), we have \(C^i(1) \in \{ 1, 2, 4\} \) by Lemma 32, so \(C^i(1) \le 4\).

Lemma 34
✓
#

Uses

Lean declarations:

The Collatz map \(C(n)\) has the closed form

\begin{equation} C(n) = \frac{(7n + 2) - (5n + 2)(-1)^n}{4} \end{equation}
14

for all \(n \in \mathbb {N}\).

Proof ▶

We split into cases based on the parity of \(n\). If \(n\) is even, then \((-1)^n = 1\), so

\begin{equation} \frac{(7n + 2) - (5n + 2)(1)}{4} = \frac{2n}{4} = \frac{n}{2} = C(n). \end{equation}
15

If \(n\) is odd, then \((-1)^n = -1\), so

\begin{equation} \frac{(7n + 2) - (5n + 2)(-1)}{4} = \frac{12n + 4}{4} = 3n + 1 = C(n). \end{equation}
16

In both cases, the formula yields \(C(n)\).