# Formal Proof Challenge: The Half-Collatz Theorem

# Table of Contents

- The Collatz Conjecture
- The Half-Collatz Theorem
- Challenge: Formally prove the Half-Collatz function to be total.

# The Collatz Conjecture

Recently I posted about an extension of Peano arithmetic (PA) called **Collatz arithmetic** (CA). CA is just like PA, except that it has the **Collatz conjecture** (CC) appended as an additional axiom. If CC is provably false in PA, then CA is inconsistent; and if CC is provably true in PA, then CA is just the same as PA. But if, as John Conway proposed, CC is **unsettleable**, then CA is a consistent proper extension of PA.

Recall the Collatz transformation *CT : N -> N*:

- if
*n*is even,*CT(n) = n/2*; - if
*n*is odd,*CT(n) = 3n + 1*;

And the Collatz loop function *C* is defined as follows:

*C(0) = 1*;*C(1) = 1*;*C(n) = C(CT(n))*;

The Collatz conjecture says that *C(n) = 1* for all *n*, or in other words, that *C* is a **total function**.

# The Half-Collatz Theorem

Note that if *n* is odd, then *3n + 1* will be even, and so every application of the odd rule will immediately be followed by an application of the even rule. This means that the odd rule can be **accelerated** slightly:

- if
*n*is odd,*CT(n) = 3k + 2*, where*n = 2k + 1*.

The Collatz loop function applies the odd and even rules until the value reaches 1, and then it terminates. Suppose instead we start from an odd number and then apply the accelerated odd rule until an even number is reached, and then stop. Will this loop function always terminate? I called this the **Half Collatz cojecture** (HCC) and proposed it as an example of a theorem that could be proved in CA but not in PA.

Well, it turns out that is not the case. Alert reader Isaac Grosof pointed out to me that **HCC was proved more than fifteen years ago**, and is in fact just a theorem of PA. I guess Half Collatz Theorem (HCT) would be a more appropriate name.

To be clear, we define the Half-Collatz transformation *HT* on odd numbers:

*HT(n = 2k + 1) = 3k + 2*.- Or equivalently,
*HT(n = 2k + 1) = n + k + 1*).

- Or equivalently,

And the Half-Collatz function *HC*:

*HC(n) = HC(HT(n))*if*n*is odd;*HC(n) = n*otherwise.

** HC is provably total**. To see why, observe this

**key fact**(which can be proved with a little algebra):

*HT(n) + 1 = (3/2)(n + 1)*(assuming*n*is odd).

Further, if *HT(n)* is still odd, then *HT(HT(n)) = (3/2)(3/2)(n + 1)*. So repeatedly applying *HT* entails repeatedly halving *n + 1*. But a number can only be halved so many times, and exactly how many is known as the number’s **2-adic valuation**. Specifically, this is the greatest *m* such that *2 ^{m}* divides

*n*.

For example:

*n = 15*.*n + 1*= 16, the 2-adic valuation of which is 4. The trajectory of repeated applications of*HT*goes: 15 -> 23 -> 35 -> 53 -> 80, which makes 4 applications.*n = 13*.*n + 1*= 14, with a 2-adic valuation of just 1. And 13 undergoes a trajectory of length 1: 13 -> 20.

In general, **the length of the trajectory of n under repeated applications of HT is exactly the 2-adic valuation of n + 1**. The 2-adic valuation function is total, and therefore so is the Half-Collatz function.

# Challenge: Formally prove the Half-Collatz function to be total.

That’s the hand-wavy natural language version of the proof. But as is well-known, constructing a **formal proof** can be quite a bit trickier. And when I say “formal proof”, I mean a proof in a programming language such as: **Lean, Coq, Idris, Agda, etc.**

The challenge here is simple (to state): **formally prove that the Half-Collatz function is total**.

I’ll lay out some basic definitions as starting points, but feel free to modify them. The language used here is Idris. I imagine that anyone who has read this far can figure out how to translate it into their own language of choice.

To say that *n* is even is just to say that there is a *k* such that *n = 2k*, and to say that *n* is odd is just to say that there is a *k* such that *n = 2k + 1*.

A handy fact is that every number is either even or odd (proof left as a warmup exercise).

Next, there is the 2-adic valuation function. I’ve implemented this with an ** assert_smaller** statement, justified because

*2/k < k*. Except when

*k = 0*; that gets the output 0 here, which is arbitrary. I’m sure there is a more elegant implementation.

After those basics, there is the Half-Collatz function itself. As usual, we define the transformation function `ht`

(defined only for odd numbers) and the looping function `halfCollatz`

. For convenience, the output of `halfCollatz`

is the list of numbers reached in its trajectory.

Last, there is the **key fact** mentioned earlier. I was able to prove a modified version of this in Idris, but the proof is tedious, long-winded, and not even a little bit enlightening. Being a merciful blogger, I spare the reader the details.

Most of these functions are accompanied by a ** total declaration**. This means that the

**totality checker**is able to verify that the function definition will always terminate one way or another. In the case of recursive functions, it must be shown that some input argument will always shrink down towards some base case.

In contrast, `halfCollatz`

is flagged as `partial`

. It is defined recursively, but the argument does not shrink. To make the challenge even more specific: **flip the partial flag to total**.