Collatz problem

DefinitionThe Collatz map#✓fully proved

The Collatz map \(T : \mathbb{N} \to \mathbb{N}\) sends a natural number \(n\) to \(n / 2\) if \(n\) is even and to \(3n + 1\) if \(n\) is odd.

def collatzStep (n : ℕ) : ℕ :=
  if n % 2 = 0 then n / 2 else 3 * n + 1
Used by 3
Used byThe accelerated Collatz map on even numbers · The accelerated Collatz map on odd numbers · Iterates of the Collatz map

DefinitionIterates of the Collatz map#✓fully proved

Let \(T : \mathbb{N} \to \mathbb{N}\) be the Collatz map, which sends \(n\) to \(n / 2\) if \(n\) is even and to \(3n + 1\) if \(n\) is odd. For natural numbers \(k\) and \(n\), the \(k\)-th Collatz iterate of \(n\) is \(T^k(n)\), the result of applying \(T\) to \(n\) exactly \(k\) times: \(T^0(n) = n\) and \(T^{k+1}(n) = T(T^k(n))\).

def collatzIterate : ℕ → ℕ → ℕ
  | 0, n => n
  | k + 1, n => collatzStep (collatzIterate k n)
Uses 1 · Used by 1
Statement usesThe Collatz map
Used byCollatz stopping time

DefinitionCollatz stopping time#✓fully proved

Let \(T : \mathbb{N} \to \mathbb{N}\) be the Collatz map, which sends \(n\) to \(n / 2\) if \(n\) is even and to \(3n + 1\) if \(n\) is odd, and let \(T^k\) denote its \(k\)-fold iterate, with \(T^0(n) = n\). For a natural number \(n\), the Collatz stopping time of \(n\) is undefined if \(n = 0\) or if \(T^k(n) \ne 1\) for every \(k \in \mathbb{N}\); otherwise it is the least \(k \in \mathbb{N}\) with \(T^k(n) = 1\).

In the Collatz literature this quantity is often called the total stopping time.

noncomputable def collatzStoppingTime (n : ℕ) : Option ℕ :=
  if n = 0 then none
  else if ∃ k : ℕ, collatzIterate k n = 1 then
    some (sInf {k : ℕ | collatzIterate k n = 1})
  else
    none
Uses 1
Statement usesIterates of the Collatz map

DefinitionDivision by \(q\) in \(\mathbb{F}_2((q))\)#✓fully proved

For a power series \(x = \sum_n x_n q^n \in \mathbb{F}_2[[q]]\), its shift is the power series \(\sum_n x_{n+1} q^n\), obtained by discarding the constant term of \(x\) and dividing by \(q\). In particular, the shift of \(qy\) is \(y\) for every \(y \in \mathbb{F}_2[[q]]\).

noncomputable def qShift (x : PowerSeries (ZMod 2)) : PowerSeries (ZMod 2) :=
  PowerSeries.mk fun n => coeff (n + 1) x
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Section 1 (the quotients x/q and (Ax+B)/q in the definition of T_{A,B}).
Used by 3
Used byThe q-analog of the 3x+1 map · The q-analog 3x+1 map on multiples of \(q\) · Dividing a multiple of \(q\) by \(q\)

TheoremDividing a multiple of \(q\) by \(q\)#✓fully proved

For every power series \(y \in \mathbb{F}_2[[q]]\), applying the shift \(\sum_n x_n q^n \mapsto \sum_n x_{n+1} q^n\) to \(qy\) gives back \(y\).

theorem qShift_X_mul (y : PowerSeries (ZMod 2)) : qShift (X * y) = y
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Section 1 (division by q).
Uses 1 · Used by 1
Statement usesDivision by \(q\) in \(\mathbb{F}_2((q))\)
Used byThe q-analog 3x+1 map on multiples of \(q\)

DefinitionThe q-analog of the 3x+1 map#✓fully proved

For a power series \(y = \sum_n y_n q^n \in \mathbb{F}_2[[q]]\), write \(y/q\) for the power series \(\sum_n y_{n+1} q^n\): the constant term of \(y\) is discarded and the rest is divided by \(q\). For power series \(A, B \in \mathbb{F}_2[[q]]\), the map \(T_{A,B} : \mathbb{F}_2[[q]] \to \mathbb{F}_2[[q]]\) is defined by \(T_{A,B}(x) = x/q\) if the constant term of \(x\) is \(0\), and \(T_{A,B}(x) = (Ax + B)/q\) otherwise.

When \(A\) and \(B\) have constant term \(1\), the numerator \(Ax + B\) has constant term \(0\) whenever \(x\) has constant term \(1\), so in that case the division by \(q\) is exact.

noncomputable def qCollatz (A B x : PowerSeries (ZMod 2)) : PowerSeries (ZMod 2) :=
  if constantCoeff x = 0 then qShift x else qShift (A * x + B)
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Section 1 (definition of T_{A,B}).
Uses 1 · Used by 11
Statement usesDivision by \(q\) in \(\mathbb{F}_2((q))\)
Used byA perturbation at \(q^{n+1}\) moves to \(q^n\) under \(T_{A,B}\) · The \(q\)-Collatz map is conjugate to the \(2\)-adic \(3x+1\) map · Fixed points and the \(2\)-cycle of the \(q\)-Collatz map · Iterates of \(T_{A,B}\) move a perturbation at \(q^{n+1}\) to \(q^{n+1-k}\) · A perturbation at \(q^n\) flips the parity of the \(n\)-th iterate · The map \(T_{1+q,1}\) is conjugate to the \(2\)-adic \(3x+1\) map · Polynomial orbits of \(T_{1,1+q^2}\) · The parity vector of the q-analog 3x+1 map · The parity vector of \(0\) · The q-analog 3x+1 map on multiples of \(q\) · Zero is a fixed point of the q-analog 3x+1 map

TheoremThe q-analog 3x+1 map on multiples of \(q\)#✓fully proved

For all power series \(A, B, y \in \mathbb{F}_2[[q]]\), the \(q\)-analog \(3x+1\) map satisfies \(T_{A,B}(qy) = y\).

theorem qCollatz_X_mul (A B y : PowerSeries (ZMod 2)) : qCollatz A B (X * y) = y
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Section 1 (definition of T_{A,B}).
Uses 3 · Used by 1
Statement usesThe q-analog of the 3x+1 map
Proof usesDivision by \(q\) in \(\mathbb{F}_2((q))\) · Dividing a multiple of \(q\) by \(q\)
Used byZero is a fixed point of the q-analog 3x+1 map

TheoremZero is a fixed point of the q-analog 3x+1 map#✓fully proved

For all power series \(A, B \in \mathbb{F}_2[[q]]\), the \(q\)-analog \(3x+1\) map satisfies \(T_{A,B}(0) = 0\).

theorem qCollatz_zero (A B : PowerSeries (ZMod 2)) : qCollatz A B 0 = 0
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Section 1 (definition of T_{A,B}).
Uses 2 · Used by 1
Statement usesThe q-analog of the 3x+1 map
Proof usesThe q-analog 3x+1 map on multiples of \(q\)
Used byThe parity vector of \(0\)

TheoremDivisibility by \(2\) from the residue modulo \(2\)#✓fully proved

If the residue modulo \(2\) of a \(2\)-adic integer \(y \in \mathbb{Z}_2\) is zero, then \(2\) divides \(y\) in \(\mathbb{Z}_2\).

theorem two_dvd_of_toZMod_eq_zero {y : ℤ_[2]} (h : PadicInt.toZMod y = 0) :
    (2 : ℤ_[2]) ∣ y
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Section 1 (parity in ℤ₂, so that T is a self-map).
Used by 3
Used byThe \(2\)-adic \(3x+1\) map · Even branch of the \(2\)-adic \(3x+1\) map · Odd branch of the \(2\)-adic \(3x+1\) map

Theorem\(3x + 1\) is even for odd \(2\)-adic \(x\)#✓fully proved

For every \(2\)-adic integer \(x \in \mathbb{Z}_2\) whose residue modulo \(2\) is nonzero, the residue of \(3x + 1\) modulo \(2\) is zero.

theorem toZMod_three_mul_add_one_of_odd {x : ℤ_[2]} (h : PadicInt.toZMod x ≠ 0) :
    PadicInt.toZMod (3 * x + 1) = 0
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Section 1 (definition of T).
Used by 3
Used byThe \(2\)-adic \(3x+1\) map · Even branch of the \(2\)-adic \(3x+1\) map · Odd branch of the \(2\)-adic \(3x+1\) map

DefinitionThe \(2\)-adic \(3x+1\) map#✓fully proved

The map \(T : \mathbb{Z}_2 \to \mathbb{Z}_2\) is defined by \(T(x) = x/2\) if \(x\) is even and \(T(x) = (3x+1)/2\) if \(x\) is odd, where even and odd refer to the residue of \(x\) modulo \(2\).

In both cases the numerator is divisible by \(2\) in \(\mathbb{Z}_2\), so the division is exact.

noncomputable def twoAdicCollatz (x : ℤ_[2]) : ℤ_[2] :=
  if h : PadicInt.toZMod x = 0 then (two_dvd_of_toZMod_eq_zero h).choose
  else (two_dvd_of_toZMod_eq_zero (toZMod_three_mul_add_one_of_odd h)).choose
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Section 1 (definition of T extended to ℤ₂).
Uses 2 · Used by 5
Statement uses\(3x + 1\) is even for odd \(2\)-adic \(x\) · Divisibility by \(2\) from the residue modulo \(2\)
Used byThe \(q\)-Collatz map is conjugate to the \(2\)-adic \(3x+1\) map · The map \(T_{1+q,1}\) is conjugate to the \(2\)-adic \(3x+1\) map · The \(2\)-adic \(3x+1\) map swaps \(1\) and \(2\) · Even branch of the \(2\)-adic \(3x+1\) map · Odd branch of the \(2\)-adic \(3x+1\) map

TheoremEven branch of the \(2\)-adic \(3x+1\) map#✓fully proved

Let \(T : \mathbb{Z}_2 \to \mathbb{Z}_2\) be the \(3x+1\) map on the \(2\)-adic integers. For every \(x \in \mathbb{Z}_2\) whose residue modulo \(2\) is zero, \(2\,T(x) = x\).

theorem two_mul_twoAdicCollatz_of_even {x : ℤ_[2]} (h : PadicInt.toZMod x = 0) :
    2 * twoAdicCollatz x = x
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Section 1 (definition of T).
Uses 3 · Used by 1
Statement usesThe \(2\)-adic \(3x+1\) map
Proof uses\(3x + 1\) is even for odd \(2\)-adic \(x\) · Divisibility by \(2\) from the residue modulo \(2\)
Used byThe \(2\)-adic \(3x+1\) map swaps \(1\) and \(2\)

TheoremOdd branch of the \(2\)-adic \(3x+1\) map#✓fully proved

Let \(T : \mathbb{Z}_2 \to \mathbb{Z}_2\) be the \(3x+1\) map on the \(2\)-adic integers. For every \(x \in \mathbb{Z}_2\) whose residue modulo \(2\) is nonzero, \(2\,T(x) = 3x + 1\).

theorem two_mul_twoAdicCollatz_of_odd {x : ℤ_[2]} (h : PadicInt.toZMod x ≠ 0) :
    2 * twoAdicCollatz x = 3 * x + 1
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Section 1 (definition of T).
Uses 3 · Used by 1
Statement usesThe \(2\)-adic \(3x+1\) map
Proof uses\(3x + 1\) is even for odd \(2\)-adic \(x\) · Divisibility by \(2\) from the residue modulo \(2\)
Used byThe \(2\)-adic \(3x+1\) map swaps \(1\) and \(2\)

TheoremThe \(2\)-adic \(3x+1\) map swaps \(1\) and \(2\)#✓fully proved

The \(2\)-adic \(3x+1\) map \(T : \mathbb{Z}_2 \to \mathbb{Z}_2\) satisfies \(T(1) = 2\) and \(T(2) = 1\).

theorem twoAdicCollatz_one_two : twoAdicCollatz 1 = 2 ∧ twoAdicCollatz 2 = 1
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Section 1 (definition of T).
Uses 3
Statement usesThe \(2\)-adic \(3x+1\) map
Proof usesEven branch of the \(2\)-adic \(3x+1\) map · Odd branch of the \(2\)-adic \(3x+1\) map

DefinitionThe parity vector of the q-analog 3x+1 map#✓fully proved

For power series \(A, B, x \in \mathbb{F}_2[[q]]\), the parity vector of \(x\) is the \(2\)-adic integer \(\mathrm{PV}_{A,B}(x) = \sum_{k \ge 0} x_k 2^k \in \mathbb{Z}_2\), where \(x_k \in \{0, 1\}\) is the constant coefficient of the \(k\)-th iterate \(T_{A,B}^k(x)\) of the \(q\)-analog \(3x+1\) map \(T_{A,B}\).

noncomputable def qCollatzParityVector (A B x : PowerSeries (ZMod 2)) : ℤ_[2] :=
  ∑' k : ℕ, ((constantCoeff ((qCollatz A B)^[k] x)).val : ℤ_[2]) * 2 ^ k
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Definition 10.
Uses 1 · Used by 3
Statement usesThe q-analog of the 3x+1 map
Used byParity vectors detect congruence modulo \(q^{n+1}\) · Parity vectors induce bijections modulo \(q^n\) · The parity vector of \(0\)

TheoremThe parity vector of \(0\)#✓fully proved

For all \(A, B \in \mathbb{F}_2[[q]]\), the parity vector of \(0\) under the \(q\)-analog \(T_{A,B}\) of the \(3x+1\) map is \(0\), that is, \(\mathrm{PV}_{A,B}(0) = 0\).

theorem qCollatzParityVector_zero (A B : PowerSeries (ZMod 2)) :
    qCollatzParityVector A B 0 = 0
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Definition 10.
Uses 3
Statement usesThe parity vector of the q-analog 3x+1 map
Proof usesThe q-analog of the 3x+1 map · Zero is a fixed point of the q-analog 3x+1 map

TheoremThe \(q\)-Collatz map is conjugate to the \(2\)-adic \(3x+1\) map#●ready to prove

Let \(A\) and \(B\) be odd power series in \(\mathbb{F}_2[[q]]\) (constant term \(1\)), let \(T_{A,B}\) be the \(q\)-analog of the \(3x+1\) map on \(\mathbb{F}_2[[q]]\), and let \(T\) be the \(3x+1\) map on the \(2\)-adic integers \(\mathbb{Z}_2\). Then there is a bijection \(h : \mathbb{Z}_2 \to \mathbb{F}_2[[q]]\) with \(h^{-1}(T_{A,B}(h(x))) = T(x)\) for every \(x \in \mathbb{Z}_2\).

public theorem_wanted qCollatz_conjugate_twoAdicCollatz (A B : PowerSeries (ZMod 2))
    (hA : constantCoeff A ≠ 0) (hB : constantCoeff B ≠ 0) :
    ∃ h : ℤ_[2] ≃ PowerSeries (ZMod 2),
      ∀ x, h.symm (qCollatz A B (h x)) = twoAdicCollatz x
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Theorem 2 (jis-2025-25.6.8-thm-2).
Uses 2
Statement usesThe q-analog of the 3x+1 map · The \(2\)-adic \(3x+1\) map

TheoremThe map \(T_{1+q,1}\) is conjugate to the \(2\)-adic \(3x+1\) map#●ready to prove

Let \(T_q = T_{1+q,1}\) be the \(q\)-analog of the \(3x+1\) map with \(A = 1 + q\) and \(B = 1\), so that \(T_q(x) = x/q\) if \(q\) divides \(x\) and \(T_q(x) = ((1+q)x + 1)/q\) otherwise, and let \(T\) be the \(3x+1\) map on the \(2\)-adic integers \(\mathbb{Z}_2\). Then there is a bijection \(h : \mathbb{Z}_2 \to \mathbb{F}_2[[q]]\) with \(h^{-1}(T_q(h(x))) = T(x)\) for every \(x \in \mathbb{Z}_2\).

public theorem_wanted qCollatz_one_add_X_conjugate_twoAdicCollatz :
    ∃ h : ℤ_[2] ≃ PowerSeries (ZMod 2),
      ∀ x, h.symm (qCollatz (1 + X) 1 (h x)) = twoAdicCollatz x
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Corollary 3 (jis-2025-25.6.8-cor-3).
Uses 2
Statement usesThe q-analog of the 3x+1 map · The \(2\)-adic \(3x+1\) map

TheoremPolynomial orbits of \(T_{1,1+q^2}\)#●ready to prove

Let \(T = T_{1,1+q^2}\) be the \(q\)-analog of the \(3x+1\) map with \(A = 1\) and \(B = 1 + q^2\). For every polynomial \(p\) over \(\mathbb{F}_2\), some iterate \(T^k(p)\) with \(k \ge 0\) lies in \(\{0, 1 + q, 1, q\}\), the set formed by the fixed points \(0\) and \(1 + q\) of \(T\) and its \(2\)-cycle \(\{1, q\}\). Moreover, for every \(x \in \mathbb{F}_2[[q]]\), \(T(x)\) is a polynomial if and only if \(x\) is a polynomial.

public theorem_wanted qCollatz_one_one_add_X_sq_polynomial :
    (∀ p : Polynomial (ZMod 2), ∃ k : ℕ,
      (qCollatz 1 (1 + X ^ 2))^[k] (p : PowerSeries (ZMod 2)) ∈
        ({0, 1 + X, 1, X} : Set (PowerSeries (ZMod 2)))) ∧
    ∀ x : PowerSeries (ZMod 2),
      (∃ p : Polynomial (ZMod 2), qCollatz 1 (1 + X ^ 2) x = p) ↔
        ∃ p : Polynomial (ZMod 2), x = p
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Theorem 5 (jis-2025-25.6.8-thm-5).
Uses 1
Statement usesThe q-analog of the 3x+1 map

TheoremA perturbation at \(q^{n+1}\) moves to \(q^n\) under \(T_{A,B}\)#●ready to prove

Let \(A, B, U, V\) be power series in \(\mathbb{F}_2[[q]]\) with \(A\), \(B\) and \(V\) odd (constant term \(1\)), let \(T_{A,B}\) be the \(q\)-analog of the \(3x+1\) map, and let \(n \ge 0\) be an integer. Then there is an odd power series \(W \in \mathbb{F}_2[[q]]\) with \(T_{A,B}(U + q^{n+1} V) = T_{A,B}(U) + q^n W\).

public theorem_wanted qCollatz_add_X_pow_mul (A B : PowerSeries (ZMod 2))
    (hA : constantCoeff A ≠ 0) (hB : constantCoeff B ≠ 0) (n : ℕ) (U V : PowerSeries (ZMod 2))
    (hV : constantCoeff V ≠ 0) :
    ∃ W : PowerSeries (ZMod 2), constantCoeff W ≠ 0 ∧
      qCollatz A B (U + X ^ (n + 1) * V) = qCollatz A B U + X ^ n * W
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Lemma 7 (jis-2025-25.6.8-lem-7).
Uses 1
Statement usesThe q-analog of the 3x+1 map

TheoremIterates of \(T_{A,B}\) move a perturbation at \(q^{n+1}\) to \(q^{n+1-k}\)#●ready to prove

Let \(A, B, U, V\) be power series in \(\mathbb{F}_2[[q]]\) with \(A\), \(B\) and \(V\) odd (constant term \(1\)), let \(T_{A,B}\) be the \(q\)-analog of the \(3x+1\) map, and let \(n\) and \(k\) be natural numbers with \(k \le n + 1\). Write \(T_{A,B}^k\) for the \(k\)-th iterate of \(T_{A,B}\). Then there is an odd power series \(W \in \mathbb{F}_2[[q]]\) with \(T_{A,B}^k(U + q^{n+1} V) = T_{A,B}^k(U) + q^{n+1-k} W\).

public theorem_wanted qCollatz_iterate_add_X_pow_mul (A B : PowerSeries (ZMod 2))
    (hA : constantCoeff A ≠ 0) (hB : constantCoeff B ≠ 0) (n : ℕ) (U V : PowerSeries (ZMod 2))
    (hV : constantCoeff V ≠ 0) (k : ℕ) (hk : k ≤ n + 1) :
    ∃ W : PowerSeries (ZMod 2), constantCoeff W ≠ 0 ∧
      (qCollatz A B)^[k] (U + X ^ (n + 1) * V) =
        (qCollatz A B)^[k] U + X ^ (n + 1 - k) * W
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Corollary 8 (jis-2025-25.6.8-cor-8).
Uses 1
Statement usesThe q-analog of the 3x+1 map

TheoremA perturbation at \(q^n\) flips the parity of the \(n\)-th iterate#●ready to prove

Let \(A, B, U, V \in \mathbb{F}_2[[q]]\) with \(A\), \(B\) and \(V\) odd (constant term \(1\)), let \(T_{A,B}\) be the \(q\)-analog of the \(3x+1\) map, and let \(n \ge 0\) be an integer. Then the \(n\)-th iterates \(T_{A,B}^n(U + q^n V)\) and \(T_{A,B}^n(U)\) have different constant terms.

public theorem_wanted qCollatz_iterate_parity_flip (A B : PowerSeries (ZMod 2))
    (hA : constantCoeff A ≠ 0) (hB : constantCoeff B ≠ 0) (n : ℕ) (U V : PowerSeries (ZMod 2))
    (hV : constantCoeff V ≠ 0) :
    constantCoeff ((qCollatz A B)^[n] (U + X ^ n * V)) ≠
      constantCoeff ((qCollatz A B)^[n] U)
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Corollary 9 (jis-2025-25.6.8-cor-9).
Uses 1
Statement usesThe q-analog of the 3x+1 map

TheoremParity vectors detect congruence modulo \(q^{n+1}\)#●ready to prove

Let \(A, B \in \mathbb{F}_2[[q]]\) be odd (constant term \(1\)), let \(\mathrm{PV}_{A,B}\) be the parity vector map of the \(q\)-analog \(T_{A,B}\) of the \(3x+1\) map, and let \(n \ge 0\) be an integer. For all \(a, b \in \mathbb{F}_2[[q]]\), we have \(\mathrm{PV}_{A,B}(a) \equiv \mathrm{PV}_{A,B}(b) \pmod{2^{n+1}}\) in \(\mathbb{Z}_2\) if and only if \(q^{n+1}\) divides \(a - b\).

public theorem_wanted qCollatzParityVector_modEq_iff (A B : PowerSeries (ZMod 2))
    (hA : constantCoeff A ≠ 0) (hB : constantCoeff B ≠ 0) (n : ℕ) (a b : PowerSeries (ZMod 2)) :
    PadicInt.toZModPow (n + 1) (qCollatzParityVector A B a) =
        PadicInt.toZModPow (n + 1) (qCollatzParityVector A B b) ↔
      X ^ (n + 1) ∣ a - b
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Theorem 11 (jis-2025-25.6.8-thm-11).
Uses 1
Statement usesThe parity vector of the q-analog 3x+1 map

TheoremParity vectors induce bijections modulo \(q^n\)#●ready to prove

Let \(A, B \in \mathbb{F}_2[[q]]\) be odd (constant term \(1\)), let \(\mathrm{PV}_{A,B}\) be the parity vector map of the \(q\)-analog \(T_{A,B}\) of the \(3x+1\) map, and let \(n \ge 1\) be an integer. Then there is a bijection \(e : \mathbb{F}_2[[q]]/(q^n) \to \mathbb{Z}/2^n\mathbb{Z}\) such that, for every \(a \in \mathbb{F}_2[[q]]\), \(e\) sends the class of \(a\) to the residue of \(\mathrm{PV}_{A,B}(a)\) modulo \(2^n\).

public theorem_wanted qCollatzParityVector_quotient_bijection (A B : PowerSeries (ZMod 2))
    (hA : constantCoeff A ≠ 0) (hB : constantCoeff B ≠ 0) (n : ℕ) (hn : 1 ≤ n) :
    ∃ e : (PowerSeries (ZMod 2) ⧸ Ideal.span {(X : PowerSeries (ZMod 2)) ^ n}) ≃ ZMod (2 ^ n),
      ∀ a, e (Ideal.Quotient.mk _ a) = PadicInt.toZModPow n (qCollatzParityVector A B a)
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Corollary 12 (jis-2025-25.6.8-cor-12).
Uses 1
Statement usesThe parity vector of the q-analog 3x+1 map

TheoremFixed points and the \(2\)-cycle of the \(q\)-Collatz map#●ready to prove

Let \(A, B \in \mathbb{F}_2[[q]]\) be odd (constant term \(1\)) and let \(T_{A,B}\) be the \(q\)-analog of the \(3x+1\) map. For every \(x \in \mathbb{F}_2[[q]]\), \(T_{A,B}(x) = x\) holds exactly when \(x = 0\) or \(x = B/(A+q)\). Moreover, for every \(x \in \mathbb{F}_2[[q]]\), \(T_{A,B}(T_{A,B}(x)) = x\) and \(T_{A,B}(x) \ne x\) hold together exactly when \(x = B/(A+q^2)\) or \(x = qB/(A+q^2)\).

public theorem_wanted qCollatz_fixedPoints_and_twoCycle (A B : PowerSeries (ZMod 2))
    (hA : constantCoeff A ≠ 0) (hB : constantCoeff B ≠ 0) :
    (∀ x, qCollatz A B x = x ↔ x = 0 ∨ x = B * (A + X)⁻¹) ∧
    ∀ x, (qCollatz A B (qCollatz A B x) = x ∧ qCollatz A B x ≠ x) ↔
      x = B * (A + X ^ 2)⁻¹ ∨ x = X * (B * (A + X ^ 2)⁻¹)
Sources
  • Kenneth G. Monks, On q-Analogs of the 3x+1 Dynamical System, Journal of Integer Sequences 28 (2025), Article 25.6.8, Lemma 13 (jis-2025-25.6.8-lem-13).
Uses 1
Statement usesThe q-analog of the 3x+1 map

TheoremNo Collatz \(m\)-cycles with \(m \le 91\) (Hercher)#●ready to prove

Let \(T\) be the shortcut Collatz map on the natural numbers, \(T(c) = c/2\) for even \(c\) and \(T(c) = (3c+1)/2\) for odd \(c\), and let \(m\) be a natural number with \(m \le 91\). There are no natural numbers \(n\) and \(p > 0\) such that \(T^i(n) > 2\) for all \(i < p\), \(T^p(n) = n\), \(T^k(n) \ne n\) for all \(k\) with \(0 < k < p\), and exactly \(m\) indices \(i < p\) satisfy both \(T^i(n) < T^{(i+1) \bmod p}(n)\) and \(T^i(n) < T^{(i+p-1) \bmod p}(n)\).

In words: no cycle of \(T\) all of whose entries exceed \(2\) (which excludes the trivial cycle \(1, 2, 1, 2, \dots\)), taken with its minimal period \(p\), has exactly \(m\) entries lying cyclically strictly below both neighbours.

public theorem_wanted no_collatz_m_cycle_le_ninety_one
    (m : ℕ) (hm : m ≤ 91) :
    ¬ ∃ n p : ℕ, 0 < p ∧
      (∀ i : ℕ, i < p →
        2 < (fun c : ℕ => if c % 2 = 0 then c / 2 else (3 * c + 1) / 2)^[i] n) ∧
      (fun c : ℕ => if c % 2 = 0 then c / 2 else (3 * c + 1) / 2)^[p] n = n ∧
      (∀ k : ℕ, 0 < k → k < p →
        (fun c : ℕ => if c % 2 = 0 then c / 2 else (3 * c + 1) / 2)^[k] n ≠ n) ∧
      (((Finset.range p).filter (fun i =>
        (fun c : ℕ => if c % 2 = 0 then c / 2 else (3 * c + 1) / 2)^[i] n <
          (fun c : ℕ => if c % 2 = 0 then c / 2 else (3 * c + 1) / 2)^[(i + 1) % p] n ∧
        (fun c : ℕ => if c % 2 = 0 then c / 2 else (3 * c + 1) / 2)^[i] n <
          (fun c : ℕ => if c % 2 = 0 then c / 2 else
            (3 * c + 1) / 2)^[(i + p - 1) % p] n)).card = m)
Sources
  • Christian Hercher, "There are no Collatz m-Cycles with m ≤ 91," Journal of Integer Sequences 26 (2023), Article 23.3.5, Main Theorem, lines 541–543, https://cs.uwaterloo.ca/journals/JIS/VOL26/Hercher/hercher5.tex with the operator at lines 104–111 and the m-cycle definition at lines 149–151.
16 fully proved10 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.