Sorry I’m a bit confused:
Are you saying that this argument showing you need more odd terms than even terms is incorrect, or are you saying that, more generally you believe that you have (or you have) an argument saying that you can’t have more odd terms than even terms?
So there is an elementary proof that there is no circuit of the form 0^l 1^k starting from x<3^k which is good to know. And the same goes for a circuit of the form 1^k 0^l starting from x<2^k, I guess.
To help finalize the above proof, you can simply invoke the fact that the multiplicative group (\mathbb{Z}/2^l\mathbb{Z})^{\rm x} is not cyclic for l \geq 3 and that the powers of 3 are a cyclic subgroup of order 2^{l-2}. From Wikipedia entry Multiplicative group of integers modulo n.
Thank you for the nice proof!! And yes, I agree for x < 2^k, I did not realise!
Sorry, Yes i was claiming i have an argument for there not being more odd terms than even, ive deleted the posts so as not to conjest the thread as im not sure my comments were relevant.
No worries, thank you!!
Inspired by our talk @mathkook @oros I’ve continued to dig for an elementary proof of no circuits and here’s something which I believe is promising.
Notations:
We know that to get a positive integer cycle, you need both:
In a circuit, we know that x_{\text{max}} = 2^l \frac{3^k - 2^k}{2^n - 3^k}, hence: x_{\text{max}} < 2^l 3^k < 3^l 3^k = 3^n.
We also know that x_{\text{max}} verifies the following congruences (note that you can ignore: this is not limited to x_{\text{max}} integer, the congruences also apply in the 2-adic and 3-adic sense, see @oros’s Q function) :
Which, by the Chinese Remainder Theorem admits exactly one positive integer solution x_0 such that x_0 < 2^n 3^k.
Note that 3^n < 2^n 3^k because \frac{3^n}{2^n 3^k} = \frac{3^l}{2^n} < \frac{3^k}{2^n} < 1 using bounds 1 and 2.
Hence x_{\text{max}} < 3^n < 2^n 3^k which implies that, in case of positive integer cycle x_{\text{max}} = x_0, i.e. x_\text{max} is exactly the unique solution x_0 < 2^n 3^k of the above system.
However, numerically solving the system for all 1 \leq l < k < 500 reveals only two cases where x_0 < 3^n which are (k,l) = (3,2) and (k,l) = (6,5):
for k in range(2,500):
for l in range(1,k):
n = k+l
A = 2**n
B = 3**k
c = crt((2**k-1)*2**l, 3**k-1, A, B)
if not (c > 3**n):
print(k,l,c,3**n)
Ouputs:
3 2 188 243
6 5 53216 177147
This gives me good hope that we can show that for (k,l) big enough, we always have x_0 > 3^n, which contradicts x_\text{max} < 3^n and x_0 = x_\text{max}.
This would then give that there are no circuits.
What do you think?
This approach seems relevant. Let us assume the well-known condition n \simeq \rho \, k with \rho = \log_2 3 for a non-trivial cycle to exist (i.e., 2^n \simeq 3^k). The values x_0 defined by the above congruences should tend to obey a uniform probability density as n increases, when properly normalized in the interval [0,2^n 3^k ]. Hence, we can estimate the probability P_n for large n that x_0 < 3^n as follows:
P_n = \cfrac{3^n}{2^n 3^k} \simeq \cfrac{3^n}{4^n} \quad (post-edit)
As the infinite series \Sigma_{n=1}^{\infty} P_n is convergent, we should expect (heuristically) the number of solutions x_0 < 3^n to be finite! Unfortunately, proving it is another story, at least without Baker theorem…
Another remark is that you do not impose n \simeq \rho \, k, so it is not clear yet if the condition l < k also leads to a finite number of solutions, but your numerical results suggest that it is the case (I checked up to k=1000) 
Using Pari/GP:
? for(k=2,1000, for(l=1,k-1, n=k+l; A=2^n; B=3^k; c=lift(chinese(Mod(-2^l,A),Mod(-1,B))); if(c<=3^n, print(k" “l” “c” "3^n))))
3 2 188 243
6 5 53216 177147
cpu time = 6,142 ms, real time = 6,143 ms.
Thank you for your analysis!!
Yes, I did a quick scan and the CRT solutions seem quite random 
I was expecting more order there…
Hence, it’s not clear at all that this approach would be simpler
T
An elementary proof of no circuits might try to show that 3^x - 2^x is never a multiple of 2^k - 3^x. We can focus on coprime k and x, since simple methods cover the rest.
Showing 2^k - 3^x always has a “spoiler” factor that 3^x - 2^x doesn’t have, that would do it.
But we seem to know very little about the divisibility properties of 2^k - 3^x when k, x are coprime.
Here’s a chaotic table along those lines.
Below, {m, {r_1 ... r_n}} means that 2^k – 3^x divided by m can never have remainders r_1, r_2 ... or r_n (for sufficiently large, coprime x and k).
{8, {1, 3}} \hspace{0.3in} 2^k – 3^x \not\equiv 1 \not\equiv 3 mod 8, for k>2
{12, {7}} \hspace{0.36in} 2^k – 3^x \not\equiv 7 mod 12, for sufficiently large k
{15, {10}}
{16, {1, 3, 9, 11}}
{20, {15}}
{21, {7, 16}}
{24, {1, 7, 11, 17, 19}}
{28, {9, 21}}
{30, {25}}
{32, {1, 3, 9, 11, 17, 19, 25, 27}}
{33, {11}}
{35, {0, 30}} \hspace{0.3in} 2^k-3^x isn’t a multiple of 35 for coprime k,x
{36, {7, 19, 31}}
{39, {4, 10, 20, 25, 26}}
{40, {1, 3, 9, 11, 15, 17, 19, 25, 27, 33, 35}}
{42, {7, 37}}
{44, {11}}
{45, {10, 25, 40}}
{48, {1, 7, 11, 17, 19, 25, 31, 35, 41, 43}}
{51, {34}}
{52, {7, 39}}
{55, {0}}
{56, {1, 3, 9, 11, 17, 19, 21, 25, 27, 33, 35, 37, 41, 43, 49, 51}}
{57, {19}}
{60, {7, 17, 19, 25, 31, 35, 43, 53, 55}}
{63, {1, 2, 4, 7, 8, 16, 28, 31, 32, 35, 37, 43, 44, 46, 49, 55, 58, 61}}
{64, {1, 3, 9, 11, 17, 19, 25, 27, 33, 35, 41, 43, 49, 51, 57, 59}}
{65, {0, 20, 26, 43, 52}}
{66, {11}}
{68, {17}}
{70, {35, 65}}
{72, {1, 7, 11, 17, 19, 25, 31, 35, 41, 43, 49, 55, 59, 65, 67}}
{73, {2, 14, 18, 20, 21, 22, 27, 30, 37, 39, 42, 44, 49, 60, 70}}
{75, {10, 25, 40, 55, 70}}
{76, {19}}
{77, {0, 44}}
{78, {25, 43, 49, 59, 65}}
{80, {1, 3, 7, 9, 11, 15, 17, 19, 25, 27, 33, 35, 41, 43, 49, 51, 53, 55, 57, 59, 63, 65, 67, 71, 73, 75, 77, 79}}
{84, {7, 19, 31, 37, 43, 49, 55, 65, 67, 77, 79}}
{85, {0, 3, 4, 8, 10, 15, 17, 18, 19, 21, 33, 35, 43, 46, 48, 49, 50, 51, 52, 56, 63, 64, 67, 70, 73, 75, 81}}
{87, {58}}
{88, {1, 3, 9, 11, 17, 19, 25, 27, 33, 35, 41, 43, 49, 51, 55, 57, 59, 65, 67, 73, 75, 81, 83}}
{90, {25, 55, 85}}
{91, {0, 2, 4, 6, 7, 8, 9, 11, 14, 15, 16, 17, 21, 22, 24, 25, 26, 27, 30, 33, 35, 39, 40, 41, 44, 49, 50, 51, 52, 55, 57, 58, 59, 60, 63, 64, 65, 69, 70, 72, 73, 74, 75, 77, 78, 79, 81, 82, 83, 85, 86, 88}}
{93, {31}}
{95, {38, 57}}
{96, {1, 7, 11, 17, 19, 25, 31, 35, 41, 43, 49, 55, 59, 65, 67, 73, 79, 83, 89, 91}}
{99, {11, 44, 77}}
{100, {15, 35, 55, 75, 95}}
So, I have a funny, even more elementary, proof of no small circuit 
which does not rely on either Bound 1 or Bound 2.
As pointed before, the small circuit question asks whether there is k,l such that the binary representation of 3^k - 1 is 1^k 0^l.
Which reformulates as the binary representation of 3^k being 1^k 0^(l-1) 1.
Using the Finite State Transducer that computes multiplication by 3 in binary (Figure 1.2)
Let’s work our way backwards (e.g. k=4, l=3):
????????
01111001
Let’s replace the ? by the bits that produce the output sequence, for k even, it gives (e.g. k=4):
...01011010011
...00001111001
The representation of the input is not finite, i.e. it is not an integer, hence not 3^{k-1}.
For k odd we have to do this twice (e.g. k=5):
...10101110001
...00001010011
...00011111001
We get that dividing by 3 twice gives a non-integer, hence not 3^{k-2}.
In above examples, l was odd. Case l even is even simpler with no need to distinguish k's parity (e.g. l=4):
...101011111011
...000011110001
And finally, case l=1 is also easy to handle: we get 3^k +1 = 2^(k+1) which only has solutions k \in {0,1}, giving 1 = 1 and 3 = 11 in binary.
All and on, no power of three (other than than 1 and 3) can be written as 1^k 0^(l-1) 1 in binary, giving the result 
But wait, by [BohmSontacchi1978], we know that an elementary bound for an integer cycle is 3^n.
Hence, it means that our maximal circuit element is of the form 3^k a + 3^k - 1 with a < 3^l. Add one to this, we get 3^k (a+1), which must end in binary by 1^k (0)^(l-1) 1.
More exactly, we have: 3^k (a+1) = 2^n a + 2^l (2^k-1) + 1 which yields (2^n - 3^k)(a+1) = 2^l - 1.
Hence we have:
(2^{k+l} - 3^k)C = 2^l - 1 with C > 1 (the case a=0 in handled by previous post)
Hence it seems there is no valid a for the thing to work and we are always in the case of a small circuit, which by previous argument (or the one before) does not exist. GPT helped me.
The argument seems correct this time but I need to revisit it tomorrow and prove in Lean
GPT gives a convincing elementary argument in the case a = 0 (i.e. 3^k - 1 = (2^k - 1)2^l), which only requires basic maths to be understood (no multiplicative FST).
Progress report:
I have the Lean proof of no small circuits (using the above GPT argument) ready (although not formulated yet in terms of Collatz cycles but just equalities of remainders):
lemma no_small_circuits
(k: ℕ)
(l: ℕ)
(hk: k > 0)
(hl: l > 0) :
((2 : ℤ)^k - 1)*2^l = (3 : ℤ)^k - 1 -> k = 1 ∧ l = 1
This Lemma says that for all k > 0 and l > 0 we have 2^l(2^k - 1) = 3^k - 1 iff (k,l) = (1,1) (this corresponds to Collatz cycle 1->2->1, which is also a circuit…).
Find the Lean proof here.
I was able to finish the proof thanks to help from the Lean Zulip.
Then I will attack the general (non small) circuit case using the argument outlined one post above
That general argument is false, key error was thinking that proving 2^{k+l} - 3^k \geq 2^{1+l} - 3 was easy. Maybe recoverable.
However, we know have an elementary proof, verified in Lean, of no small circuits which is already cool
Here is a promising, elementary proof of 2^{k+l} - 3^k \geq 2^{1+l} - 3, which was the broken step of the argument for no big circuits.
I’m checking it thoroughly by hand then will Leanify.
In this restricted case, I poked GPT to see if you need Baker’s full argument or if you could get away with something weaker, using only part of Baker’s proof and it seems you can (would have to be carefully checked):
i.e. no algebraic geometry needed in our case + going for a far less tight bound than Baker’s
In some sense, it could mean the resulting argument is relatively elementary, but again, careful inspection required.
If we pursue along these lines, we may end up with an “elementary” proof that is much more complicated (for a human reader) than the non-elementary proof based on Baker-like results. On the other hand, this kind of proof may be easier to formalize in a computer language, which I suppose is what you want.
A closer look reveals that the elementary bound in (D) is very weak. Probably not sufficient for what is needed to conclude the no-circuit proof.
