The Collatz bijection

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-02-10.
Last modified on 2023-10-16.

module elementary-number-theory.collatz-bijection where
Imports 
open import elementary-number-theory.distance-natural-numbers
open import elementary-number-theory.euclidean-division-natural-numbers
open import elementary-number-theory.modular-arithmetic
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.coproduct-types
open import foundation.identity-types

Idea

We define a bijection of Collatz

Definition

cases-map-collatz-bijection : (n : ℕ) (x : ℤ-Mod 3) (p : mod-ℕ 3 n ＝ x) → ℕ
cases-map-collatz-bijection n (inl (inl (inr _))) p =
  quotient-euclidean-division-ℕ 3 (2 *ℕ n)
cases-map-collatz-bijection n (inl (inr _)) p =
  quotient-euclidean-division-ℕ 3 (dist-ℕ (4 *ℕ n) 1)
cases-map-collatz-bijection n (inr _) p =
  quotient-euclidean-division-ℕ 3 (succ-ℕ (4 *ℕ n))

map-collatz-bijection : ℕ → ℕ
map-collatz-bijection n = cases-map-collatz-bijection n (mod-ℕ 3 n) refl

Recent changes