On A057985 and A287066

Question

• Let $a(n)$ be A057985 (i.e., start with $0$ and repeatedly substitute: $0 \to 01$, $1 \to 12$, $2 \to 0$).

• Let $b(n)$ be A287066 (i.e., start with $1$ and repeatedly substitute: $0 \to 01$, $1 \to 12$, $2 \to 0$).

• Let $c(n)$ be A005314. Here

$$ c(n) = 2c(n-1) - c(n-2) + c(n-3), \\ c(0) = 0, c(1) = 1, c(2) = 2 $$

• Let $d(n)$ be an integer sequence such that

$$ d(n) = \sum\limits_{i=1}^{n} c(i) $$

• Let $e(n)$ be the smallest number $k$ such that $c(k)>n$.

• Let $f(n)$ be the smallest number $q$ such that $d(q)>n$.

I conjecture that

$$ a(n) = b(n - d(f(n-2) - 1) - 1), \\ a(1) = 0, a(2) = 1, \\ b(n) = a(n - c(e(n-1) - 1)), \\ b(1) = 1, b(2) = 2 $$

Here is the PARI/GP program to check it numerically:

a_upto(n) = my(A = 2, B = 2, v1); v1 = vector(n+1, i, 0); v1[2] = 1; while(B<n, if(v1[A]==2, v1[B+1] = 0, v1[B+1] = v1[A]; v1[B+2] = v1[A] + 1; B++); A++; B++); v1 = vector(n, i, v1[i])
b_upto(n) = my(A = 2, B = 2, v1); v1 = vector(n+1, i, 0); v1[1] = 1; v1[2] = 2; while(B<n, if(v1[A]==2, v1[B+1] = 0, v1[B+1] = v1[A]; v1[B+2] = v1[A] + 1; B++); A++; B++); v1 = vector(n, i, v1[i])
f1(n) = if(n == 1, 2, my(A = solve(r=0, 1, r*(2 - r + r^2)-1)); ceil(log((19*A - A^2 + 11*A^3)/(23*n))/log(A)))
f2(n) = my(A = f1(n) + 1, v1); v1 = vector(A, i, 0); v1[2] = 1; v1[3] = 2; for(i = 4, A, v1[i] = 2*v1[i-1] - v1[i-2] + v1[i-3]); while(!(v1[A] > n), v1 = concat(v1, 2*v1[A] - v1[A-1] + v1[A-2]); A++); v2 = v1; for(i = 2, A, v2[i] += v2[i-1]); [v1, v2]
a1(n) = my(v1, v2); v1 = f2(n); v2 = v1[2]; v1 = v1[1]; my(A = #v1, B = A, C = 0); while(n > 2, if(!(C%2), while(v2[A] > (n-2), A--); n -= v2[A] + 1, while(v1[B] > (n-1), B--); n -= v1[B]); C++); n + C%2 - 1
b1(n) = my(v1, v2); v1 = f2(n); v2 = v1[2]; v1 = v1[1]; my(A = #v1, B = A, C = 0); while(n > 2, if(C%2, while(v2[A] > (n-2), A--); n -= v2[A] + 1, while(v1[B] > (n-1), B--); n -= v1[B]); C++); n - C%2
test1(n) = vector(n, i, a1(i)) == a_upto(n)
test2(n) = vector(n, i, b1(i)) == b_upto(n)

Is there a way to prove it?

Answer 1

This is something that can be proved (in principle) with Walnut, a system for automatically proving results like this. You would have to use a special Pisot numeration system, the P4 system, as discussed in my paper here: https://www.rairo-ita.org/articles/ita/abs/2023/01/ita220038/ita220038.html .

It would probably take me a couple of hours to get all the details down correctly, and run the Walnut code, so before I do so, please contact me by e-mail (easily findable with google search of my name) and tell me more about why you're interested in the problem.

Update: OK, now I have verified the claims. (Thanks to Zack Wolske for pointing out my previous misunderstanding of the definition.) Here is a sketch of the proof; I can provide more details to anyone interested.

I'm working with the P4 numeration system discussed the paper I cited, which expresses every natural number as a sum of distinct elements of the sequence 1, 2, 4, 7, 12, 21, 37, 65, 114, 200,... which satisfies the same linear recurrence as the one in the original question. To make this representation unique, we require that we never use three consecutive terms (like 2+4+7), or two consecutive terms and then an additional term one more index away (like 12+7+2).

In this numeration system, the addition relation x+y=z, and the set of all valid representations, are both recognized by finite automata and so, as shown in my book The Logical Approach to Automatic Sequences, there is a decision procedure for the first-order theory with addition.

In particular, there is an automaton of 53 states that takes $n$ expressed in this numeration system and computes $a(n)$, and similarly for $b(n)$. Similarly, there is an automaton that recognizes the representation of the pairs $(c(n),d(n))$, and hence there are automata for $d(f(n)-1)$ and $c(e(n)-1)$. We can then write first-order logical formulas for the assertions of the original question, and the Walnut system returns TRUE for both. So the results are rigorously proved.