Terras Theorem

Stream: Is there code for X?

[Wouter Smeenk]

Is there a Lean proof for the Terras Theorem. The Theorem is about the Collatz sequences. I found this page on it: http://www.ericr.nl/wondrous/terras.html

[Johan Commelin]

I'm 99% sure that this proof has not been formalized in Lean.

[Junyan Xu]

Note Tao's stronger result (blog, Quanta) from 2019:
image.png

[Thomas Vigouroux]

I've been fiddling a little with the proof provided in the article above, but for now I am unable to simply prove the first lemma (which is stated to be simple).

Did you make any progress on your side ?

[Mario Carneiro]

It looks easy enough to me, what is your progress?

[Thomas Vigouroux]

Well I realized I was interepreting the "first k elements" wrong, because the sequence is starting at 0

The lemma I am trying to prove is the following:

lemma First (a b k: ℕ): b < 2^(k + 1) → n = a * 2^(k + 1) + b → Parity n k = Parity b k := by induction k with ...

[Thomas Vigouroux]

I just did the base case, now it's time for the induction

[Thomas Vigouroux]

And I define the following:

import Mathlib.Tactic

@[simp]
def Syr (n: ℕ): ℕ :=
  if Even n then
    n / 2
  else
    (3 * n + 1) / 2

@[simp]
def Glide (n i: ℕ): ℕ := Syr^[i] n

@[simp]
def Parity (n i: ℕ): ℕ := (Glide n i) % 2

[Mario Carneiro]

I think you want to strengthen the lemma statement to say

lemma First (a b k i : ℕ) : b < 2^k → i < k → Parity (a * 2^k + b) i = Parity b i :=

[Thomas Vigouroux]

Well I wondered if it was necessary though, because the first version, implies the second by induction too (I think ?)

[Mario Carneiro]

Yes they are all true and hence equivalent, but this version is closer to the statement and also likely easier to prove by induction

[Mario Carneiro]

Once you have the proof it is easier to see whether it can be simplified

[Thomas Vigouroux]

Okay, so I have done some progress, but I am kind of stuck, and I think I am misunderstanding something, may I ask for help ?

Basically, the two sorry are where I am stuck, the goal resembles one of the hypothesis, but I quite cannot firugre out how to use them...

Here is the code:

import Mathlib.Tactic

@[simp]
def Syr (n: ℕ): ℕ :=
  if Even n then
    n / 2
  else
    (3 * n + 1) / 2

@[simp]
def Glide (n i: ℕ): ℕ := Syr^[i] n

@[simp]
def Parity (n i: ℕ): ℕ := (Glide n i) % 2

lemma First (a b k: ℕ): b < 2^(k + 1) → Parity (a * 2^(k+1) + b) k = Parity b k := by {
  apply Nat.case_strong_induction_on k
  · simp
    intro hb
    rw [Nat.add_comm, Nat.add_mul_mod_self_right]
  · intro k hyp hb
    have hb1 : (a * 2^(k.succ + 1) + b) % 2 = b % 2
    {
    calc (a * 2^(k.succ + 1) + b) % 2
      _ = (a * 2^(k + 2) + b) % 2 := by exact rfl
      _ = (a * 2^(k + 2) % 2 + b % 2) % 2 := by exact Nat.add_mod (a * 2 ^ (k' + 2)) b 2
      _ = b % 2 := by {
        have ha: a * 2^(k + 2) % 2 = 0
        · rw [Nat.mul_mod, Nat.pow_mod]
          simp
        rw [ha]
        simp
      }
    }

    have hb' : Even (a * 2^(k.succ + 1) + b) ↔ Even b
    · repeat rw [Nat.even_iff]
      rw [hb1]

    by_cases h : Even b
    · unfold Parity at *
      unfold Glide at *
      rw [Function.iterate_succ, Function.comp, Function.comp, Syr, Syr]
      rw [if_pos h, if_pos (hb'.2 h)]
      sorry
    · unfold Parity at *
      unfold Glide at *
      rw [Function.iterate_succ, Function.comp, Function.comp, Syr, Syr]
      rw [if_neg h, (if_neg ((not_iff_not.2 hb').2 h))]
      sorry
}

[Alex J. Best]

I'm not 100% sure, but it seems to me generalizing the induction over b is the way to go, like so

import Mathlib.Tactic

@[simp]
def Syr (n: ℕ): ℕ :=
  if Even n then
    n / 2
  else
    (3 * n + 1) / 2

@[simp]
def Glide (n i: ℕ): ℕ := Syr^[i] n

@[simp]
def Parity (n i: ℕ): ℕ := (Glide n i) % 2

lemma First (a b k: ℕ): b < 2^(k + 1) → Parity (a * 2^(k+1) + b) k = Parity b k := by {
  revert b
  apply Nat.case_strong_induction_on k
  · intro b
    simp
    intro hb
    rw [Nat.add_comm, Nat.add_mul_mod_self_right]
  · intro k hyp b hb
    have hb1 : (a * 2^(k.succ + 1) + b) % 2 = b % 2
    {
    calc (a * 2^(k.succ + 1) + b) % 2
      _ = (a * 2^(k + 2) + b) % 2 := by exact rfl
      _ = (a * 2^(k + 2) % 2 + b % 2) % 2 := by exact Nat.add_mod (a * 2 ^ (k' + 2)) b 2
      _ = b % 2 := by {
        have ha: a * 2^(k + 2) % 2 = 0
        · rw [Nat.mul_mod, Nat.pow_mod]
          simp
        rw [ha]
        simp
      }
    }

    have hb' : Even (a * 2^(k.succ + 1) + b) ↔ Even b
    · repeat rw [Nat.even_iff]
      rw [hb1]

    by_cases h : Even b
    · unfold Parity at *
      unfold Glide at *
      rw [Function.iterate_succ, Function.comp, Function.comp, Syr, Syr]
      rw [if_pos h, if_pos (hb'.2 h)]
      rw [Nat.add_div_of_dvd_left]
      rw [pow_succ', show a * (2 ^ (k + 1) * 2) / 2 = a * 2 ^ (k + 1) by sorry]
      rw [hyp] --works at least
    · unfold Parity at *
      unfold Glide at *
      rw [Function.iterate_succ, Function.comp, Function.comp, Syr, Syr]
      rw [if_neg h, (if_neg ((not_iff_not.2 hb').2 h))]
      sorry
}

[Thomas Vigouroux]

Yep I've been able to do that by slightly changing the definition of the lemma, generalizing over a and b

[Thomas Vigouroux]

Though I am now stuck at the proof of the Odd b case, strangely

[Thomas Vigouroux]

(by the way, I just learned about the show function, nice)

[Thomas Vigouroux]

I think that the version of the lemma provided in the blog post above is slightly to specific, and that the version in the original Terras paper here is seasier to prove.

It uses n = m [MOD 2^k] instead of the notation above, which seems a little too restrictive