[seqfan] More about lex earliest cubefree 0,1 sequence

[Neil Sloane]

Dear Seqfans, At the beginning of May there were several messages here
about this sequence A282317.  The entry now contains the following
 nonconstructive existence proof:

Construct the infinite complete binary tree, with the root labeled with the
null symbol,
the two nodes on the next level up labeled 0, 1. the four nodes on the
second level up labeled 0, 1. 0, 1, and so on.
Any infinite binary string specifies an infinite path P starting at the
root, and a path P is lexicographically earlier than a path Q iff P is to
the left of Q.
Color all infinite paths starting at the root and corresponding to cubefree
strings red.
There certainly are infinite red paths, for example those corresponding to
the Thue-Morse sequence A010060 and its complement.
Start at the root, and at each step take the left-most red edge. There is
always at least one choice and at most two. The resulting sequence is
A282317.  QED

The entry A282317 gives 10000 terms, starting
0, 0, 1, 0, 0, 1, 0, 1, 0, 0, 1, 0, 0, 1, 1, 0, 0, 1, 0, 0, 1, 0, 1, 0, 0,
1, ...
but there is no proof that this is correct.

The initial 0 is correct, because there IS an infinite cubefree sequence
beginning with 0, namely the Thue-Morse sequence T = 01101001...

I claim that the first 6 terms are correct, because the sequence S = 0010T
= 001001101001...  = PT is cubefree, where we have added a prefix P = 0010
to T.
Proof:
The starting point is the fact (Allouche and Shallit, Automatic Seqs., pp.
14-15)
that T is not only cubefree, it is overlap-free, meaning there is no
substring of the form ABABA, where B is a binary string and A is 0 or 1.
Suppose now that S is not cubefree. Then the cube X must involve P.
Case 0: the cube starts at the beginning of S, so we have
S = XXX... , and we can check that the length of X is at least 5, so suppose
X=0010abc...f. Then
S = 0010abc...f0010abc...f0010abc...f...
which means
T = abc...f0010abc...f0010abc...f... = ABABA... where A=a,
B = bc...f0010, so T is not overlap-free, a contradiction.
There is a similar argument if X starts at the 2nd, 3rd, or 4th symbol of
S. QED

The question is, can this argument be extended to prove that more
terms of A282317 are correct?  That is, let W denote the first k terms of
A282317, can we construct an infinite cubefree sequence that begins with
W?  That would prove the first k terms of A282317 are correct.