Defining the Collatz function of the 2-adic integers

Stream: general

[Tristan Stérin]

Hello,

I am very new to lean and I'm trying to define the Collatz function over the 2-adic integers:

import Mathlib.NumberTheory.Padics.PadicIntegers

def C_Z2 (x : ℤ_[2]) : ℤ_[2] :=
  if (x : ZMod 2) = 0 then x / 2 else 3 * x + 1

This fails with:

type mismatch
  x
has type
  ℤ_[2] : Type
but is expected to have type
  ZMod 2 : Type

failed to synthesize
  HDiv ℤ_[2] ℕ ℤ_[2]

Would you know how to fix these issues? Thank you!

[Kenny Lau]

@Tristan Stérin welcome! for a MWE, pleaes include the relevant imports etc. so that your code compiles as it is (if you hover over the code block, you can click the button on the top right corner to be transported to online Lean, so that you can confirm)

[Kenny Lau]

from these error messages, the first error is saying that it can't figure out a way to convert an element of Z_2 to an element of Z/2Z yet; the second error is saying that obviously x/2 is not defined on Z_2

[Kenny Lau]

when mathematicians write down an expression x/y, it usually means, "assume x is divisible by y, and then evaluate this expression"; but a computer can't do that, whatever expression you write down will already have a meaning

[Kenny Lau]

so if you ever write down the expression "x / 2", then you're making a promise that this expression will make sense for every x : Z_[2]

[Tristan Stérin]

Apologies, I'm using mathlib's Mathlib.NumberTheory.Padics.PadicIntegers

[Tristan Stérin]

Any even 2-adic integer x ends with LSB 0 and operation x/2 only consists in getting rid of this final 0. I assume this logic is encoded somewhere in mathlib.

[Kenny Lau]

Tristan Stérin said:

Any even 2-adic integer x ends with LSB 0

This is an "implementation-dependent" statement.

[Kenny Lau]

anyways, here is how you do it, given the current implementation

[Kenny Lau]

@Tristan Stérin Z_[2] is defined to be elements of ℚ_[2] with norm <= 1. show that under your assumptions, (↑x : ℚ_[2]) / 2 has norm <= 1, then use that to get back your answer

[Tristan Stérin]

Thank you!

[Yakov Pechersky]

import Mathlib.NumberTheory.Padics.PadicIntegers
import Mathlib.NumberTheory.Padics.RingHoms

lemma PadicInt.norm_le_one_div_p_of_mem_maximalIdeal {p : ℕ} [Fact p.Prime] {x : ℤ_[p]}
    (hx : x ∈ IsLocalRing.maximalIdeal ℤ_[p]) :
    ‖(x : ℚ_[p]) / p‖ ≤ 1 := by
  sorry

noncomputable
def C_Z2 (x : ℤ_[2]) : ℤ_[2] :=
  if hx : x.toZMod = 0
    then ⟨x / 2, x.norm_le_one_div_p_of_mem_maximalIdeal (by simp [← PadicInt.ker_toZMod, hx])⟩
    else 3 * x + 1

[Tristan Stérin]

Thank you !! This hints thay I may need to define them differently for my needs (and maybe prove that both definitions are the same)

[Kenny Lau]

in type theory, everything has to have a type immediately

[Kenny Lau]

if you think about it more, you'll realise that in maths "x/y" can have an indeterminate type until x and y are specified :slight_smile:

[Kenny Lau]

for example, people will say that x/y is "undefined" when y=0

[Kenny Lau]

and 13/4 is "a rational number" even though you started with natural numbers 13 and 4

[Kenny Lau]

so you must be careful when translating these expressions into Lean

[Jz Pan]

Cheat:

import Mathlib.NumberTheory.Padics.PadicIntegers

noncomputable def C_Z2 (x : ℤ_[2]) : ℤ_[2] :=
  open scoped Classical in
  if h : 2 ∣ x then h.choose else 3 * x + 1

[Yakov Pechersky]

That's basically what docs#PadicInt.zmodRepr does too.

[Yakov Pechersky]

It can probably be made computable by switching to Nat.find

[Kenny Lau]

Yakov Pechersky said:

It can probably be made computable by switching to Nat.find

uh.... Qp is defined using Cauchy sequences. Let f: N -> Q be the sequence such that f(n) = 0 if the Riemann Hypothesis is true, and f(n) = 1 if the Riemann Hypothesis is false. What's the corresponding value of zmodRepr?

[Yakov Pechersky]

https://hal.science/hal-01444183/document

[Kenny Lau]

sorry, this f is not computable, but you can convert RH into a Π1 statement basically of the form ∀ n, f(n) < g(n) for functions f, g : ℕ → ℚ, then you can instead form the Cauchy sequence a_k that is 1 if that statement is true for all n < k, and 0 otherwise

[Kenny Lau]

Yakov Pechersky said:

https://hal.science/hal-01444183/document

sure, you can cite articles, but have you read the fine print? did you see that they're using a different definition? did you look at all the merits and weaknesses of the alternate definition?

[Kenny Lau]

it's the same situation with the reals

[Kenny Lau]

there are "more computable definitions" but none of them is perfect

[Kenny Lau]

and i don't think mathlib cares about these more computable definitions

[Yakov Pechersky]

Yes, but if someone wants to work on Collatz, they might be interested in actually "computing" a chain

[Kenny Lau]

well anyone is welcome to make an alternate definition of Z_[p] anywhere