Collatz step differences

The question

conjecture1. Conjecture 1: More than half of the terms are 0.

• _Ya-Ping Lu_, May 04 2024

conjecture2. Conjecture 2: 1, 6 and 16 appear only once and 3 appears twice in the sequence, i.e., $a(1)=1$, $a(2)=6$, $a(4)=a(5)=3$, and $a(8)=16$.

• _Ya-Ping Lu_, May 04 2024

conjecture3. Conjecture 3 (Ya-Ping Lu, 2024): Except 1, 3 and 6, the absolute value of all terms can be written as $5x+8y$ for $x,y\in \mathbb{N}$. (Note: in the OEIS comment, "x and y are integers" means $x$ and $y$ have the same sign, i.e., $|v|=5x+8y$ with $x,y\ge 0$, since every integer is a $\mathbb{Z}$-linear combination of 5 and 8).

conjecture4. Conjecture 4 (Ya-Ping Lu, 2024): For an $m$ that appears in the sequence, the ratio of the number of terms with value $m$ to that of $-m$ approaches 1 as $n\to \infty$, for any $|m|\notin \{1,3,6,16\}$.

Differences in adjacent elements of the sequence quantifying the steps needed for $n$ to converge to 1 in the Collatz Conjecture. $$a(n)=A006577(n+1)-A006577(n)$$ for $n>0$.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.OEIS.«153330» (4 statements).

theorem conjecture1 :
    1 / 2 < Filter.atTop.liminf (fun n : ℕ ↦
      (((Finset.Icc 1 n).filter (fun i ↦ a i = some 0)).card : ℝ) / (n : ℝ))

theorem conjecture2 :
    indices 1 = {1} ∧
    indices 6 = {2} ∧
    indices 16 = {8} ∧
    indices 3 = {4, 5}

theorem conjecture3 (n : ℕ) (v : ℤ) (hn : 0 < n) (ha : a n = some v)
    (hv : v ≠ 1 ∧ v ≠ 3 ∧ v ≠ 6) :
    ∃ x y : ℕ, v.natAbs = 5 * x + 8 * y

theorem conjecture4 (m : ℤ) (hm : m.natAbs ∉ ({1, 3, 6, 16} : Finset ℕ))
    (hocc : ∃ n, 0 < n ∧ a n = some m) :
    Filter.atTop.Tendsto
      (fun n : ℕ ↦
        (((Finset.Icc 1 n).filter (fun i ↦ a i = some m)).card : ℝ) /
        (((Finset.Icc 1 n).filter (fun i ↦ a i = some (-m))).card : ℝ))
      (nhds 1)

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• A153330

Source and licence

Imported from Formal Conjectures (OEIS), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.