Inevitably for any amateur mathematician, I've been playing with the Collatz Conjecture. I have found it's easier to examine and to generate theorems if we use this equivalent statement:
$$c_{n+1}\equiv\begin{cases} \begin{array}{c} \frac{c_{n}}{2};\;c_{n}\in \; Even\\ \frac{3c_{n}+1}{2};\;c_{n}\in \; Odd \end{array}\end{cases}$$
and
$$\forall \{c_{0}>1\}\;\exists\; z\;\text { s.t.}\; c_{z}<c_{0}$$
In other words, I only prove that the series drops below its initial value. This is true iff the Collatz Conjecture is true.
Let's further define: $L(c_{0})$ as the number of steps this takes. For example $L(11)=5$ because $c_{n<5}\geqq11$ and $c_{5}<11$ $$11\rightarrow17\rightarrow26\rightarrow13\rightarrow20\rightarrow10$$
So here's my problem: When I binned up values of $L(c_{0})$ for lots of starting values, I found that there seem to be no values of $c_{0}$ where $L(c_{0})\epsilon\{3,6,9,11,14,17,19,22,25,28,...\}$. The members of this series have the form $1+\Big\lfloor\frac{n}{1-\frac{ln2}{ln3}}\Big\rfloor$. I googled the series and found the link below which says “These numbers appear in connection with the 3x+1 problem.”
But I haven't been able to prove this theorem or find any discussion of connection online.
So, how would we prove this theorem, that there exist no $c_{0}$ s.t. $L(c_{0})=1+\Big\lfloor\frac{n}{1-\frac{ln2}{ln3}}\Big\rfloor$ for integer n?
It's easy enough to prove for small values. For example, a Mathematica script will quickly verify that for values of the form $8m+{0,1,2,3,4,5,6,7}$, $L(c_{0})$ is indeed either <3 or >3, never =3. But done this way, the proof scales up in powers of 2. Is it possible to prove it in general?
Mike Winkler on arXiv "Mike Winkler - The algorithmic structure of the finite stopping time behavior of the 3x + 1 function" (arxiv.org/abs/1709.03385) has a lot of material, I think he has also a proof for the floor()-formula that you refer to.