def Collatz.collatz (n : ℕ) : ℕ

The Collatz function: n/2 if n is even, 3n+1 if n is odd.

Equations

• Collatz.collatz n = if n % 2 = 0 then n / 2 else 3 * n + 1

def Collatz.CollatzConverges (n : ℕ) : Prop

A natural number converges under the Collatz function if some iterate equals 1.

Equations

• Collatz.CollatzConverges n = ∃ (k : ℕ), Collatz.collatz^[k] n = 1

noncomputable def Collatz.stoppingTime (n : ℕ) (h : CollatzConverges n) : ℕ

The stopping time of n: the minimal k such that collatz^[k] n = 1.

Equations

• Collatz.stoppingTime n h = Nat.find h

theorem Collatz.stoppingTime_spec (n : ℕ) (h : CollatzConverges n) : collatz^[stoppingTime n h] n = 1

theorem Collatz.stoppingTime_min (n : ℕ) (h : CollatzConverges n) (k : ℕ) (hk : collatz^[k] n = 1) : stoppingTime n h ≤ k