# Rudin-Shapiro Sums Via Automata Theory and Logic

Narad Rampersad111Research funded by a grant from NSERC, 2019-04111.
Dept. of Mathematics and Statistics
University of Winnipeg
Winnipeg, MB R2B 2E9
Canada
<EMAIL_ADDRESS>
Jeffrey Shallit222Research funded by a grant from NSERC, 2018-04118.
School of Computer Science
University of Waterloo
Waterloo, ON N2L 3G1
Canada
<EMAIL_ADDRESS>

###### Abstract

We show how to obtain, via a unified framework provided by logic and automata
theory, many classical results of Brillhart and Morton on Rudin-Shapiro sums.
The techniques also facilitate easy proofs for new results.

##  1 Introduction

The Rudin-Shapiro coefficients

$(a(n))_{n\geq 0}=(1,1,1,-1,1,1,-1,1,\ldots)$

form an infinite sequence of $\pm 1$ defined recursively by the identities

$\displaystyle a(2n)$ $\displaystyle=a(n)$ $\displaystyle a(2n+1)$
$\displaystyle=(-1)^{n}a(n)$

and the initial condition $a(0)=1$. It is sequence A020985 in the On-Line
Encyclopedia of Integer Sequences (OEIS) [25]. It was apparently first
discovered by Golay [10, 11], and later studied by Shapiro [24] and Rudin
[20]. The map $a(n)$ can also be defined as $a(n)=(-1)^{r_{n}}$, where $r_{n}$
counts the number of (possibly overlapping) occurrences of $11$ in the binary
representation of $n$ [3, Satz 1].

The Rudin-Shapiro coefficients have many intriguing properties and have been
studied by many authors; for example, see [1, 4, 9, 17, 18]. They appear in
number theory [16], analysis [13], combinatorics [14], and even optics [10,
11], just to name a few places.

In a classic paper from 1978, written in German, Brillhart and Morton [3]
studied sums of these coefficients, and defined the two sums333One can make
the case that these definitions are “wrong”, in the sense that many results
become significantly simpler to state if the sums are taken over the range
$0\leq i<n$ instead. But the definitions of Brillhart-Morton are now very
well-established, and using a different indexing would also make it harder to
compare our results with theirs.

$\displaystyle s(n)$ $\displaystyle=\sum_{0\leq i\leq n}a(i)$ (1)
$\displaystyle t(n)$ $\displaystyle=\sum_{0\leq i\leq n}(-1)^{i}a(i).$ (2)

The first few values of the functions $s$ and $t$ are given in Table 1. They
are sequences A020986 and A020990 respectively, in the OEIS.

$n$ | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | 16 | 17 | 18 | 19 | 20
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
$s(n)$ | 1 | 2 | 3 | 2 | 3 | 4 | 3 | 4 | 5 | 6 | 7 | 6 | 5 | 4 | 5 | 4 | 5 | 6 | 7 | 6 | 7
$t(n)$ | 1 | 0 | 1 | 2 | 3 | 2 | 1 | 0 | 1 | 0 | 1 | 2 | 1 | 2 | 3 | 4 | 5 | 4 | 5 | 6 | 7
Table 1: First few values of $s(n)$ and $t(n)$.

A priori it is not even clear that these sums are always non-negative, but
Brillhart and Morton proved that they are, and also proved many other
properties of them. Most of these properties can be proved by induction,
sometimes rather tediously.

In this paper we show how to replace nearly all of these inductions with
techniques from logic and automata theory. Ultimately, almost all the
Brillhart-Morton results444The main exceptions are the results about the limit
points of $s(n)/\sqrt{n}$ and $t(n)/\sqrt{n}$ in [3]. can be proved in a
simple, unified manner, simply by stating them in first-order logic and
applying the Walnut theorem-prover [19, 22]. In fact, there are basically only
three simple inductions in our entire paper. One is the brief induction used
to prove Lemma 19. The other two are the inductions used in Theorem 1 to prove
the correctness of our constructed automata, and in these cases the induction
step itself can be proved by Walnut! We are also able to easily derive and
prove new results; see Section 9.

Finally, another justification for this paper is that the same techniques can
easily be harnessed to handle related sequences; for example, see [23].

The paper is organized as follows: Section 2 gives basic notation used in
describing base-$b$ expansions. Section 3 gives the automata computing the
functions $s(n)$ and $t(n)$ and justifies their correctness. In Section 4 we
begin proving the results of Brillhart and Morton using our technique, and
illustrate the basic ideas, and this continues in Section 5. In Section 6 we
show how to compute various special values of $s$ and $t$. Then in Section 7,
we obtain the deepest results of Brillhart and Morton, on inequalities for the
Rudin-Shapiro sums. In Section 8 we illustrate how our ideas can be used to
enumerate some quantities connected with $s(n)$. In Section 9 we use our
technique to prove various new results about the Rudin-Shapiro sums. In
Section 10 we prove properties about a space-filling curve associated with $s$
and $t$. Finally, in Section 11, we explain how the technique can be used to
prove properties of two analogues of the Rudin-Shapiro sums.

We assume the reader is familiar with the basics of automata and regular
expressions, as discussed, for example, in [12].

##  2 Notation

Let $b\geq 2$ be an integer, and let $\Sigma_{b}$ denote the alphabet
$\\{0,1,\ldots,b-1\\}$.

For a string $x\in\Sigma_{b}^{*}$, we let $[x]_{b}$ denote the integer
represented by $x$ in base $b$, with the more significant digits at the left.
That is, if $x=c_{1}c_{2}\cdots c_{i}$, then $[x]_{b}:=\sum_{1\leq j\leq
i}c_{j}b^{i-j}$. For example, $[00101011]_{2}=[223]_{4}=43$.

For an integer $n\geq 0$, we let $(n)_{b}$ denote the canonical base-$b$
representation of $n$, starting with the most significant digit, with no
leading zeros. For example, $(43)_{2}=101011$. We have $(0)_{b}=\epsilon$, the
empty string.

##  3 Automata and logic

Walnut is free software, originally designed by Hamoon Mousavi, that can
rigorously prove propositions about automatic sequences [19, 22]. If a
proposition $P$ has no free variables, one only has to state it in first-order
logic and then the Walnut prover will prove or disprove it (subject to having
enough time and space to complete the calculation)555In fact, all the Walnut
code in this paper runs in a matter of milliseconds.. If the proposition $P$
has free variables, the program computes a finite automaton accepting exactly
the values of the free variables that make $P$ evaluate to true.

Because of these two features, there is a philosophical choice in using
Walnut. Either we can state the desired result as a first-order logical
formula and verify it, or, if the theorem involves characterizing a set of
numbers $n$ with a certain property, we can simply create a formula with $n$
as a free variable, and consider the resulting automaton as the desired
characterization. In this case, if the automaton is simple enough, we can find
a short regular expression specifying the accepted strings, and then interpret
it as a function of $n$ in terms of powers of the base $b$. The former is most
appropriate when we already know the statement of the theorem we are trying to
prove; the latter when we do not yet know the precise characterization that
will eventually become a theorem. In this paper we have used both approaches,
to illustrate the ideas.

As is well-known, the Rudin-Shapiro sequence is $2$-automatic and therefore,
by a classic theorem of Cobham [8], also $4$-automatic. This means there is a
deterministic finite automaton with output (DFAO) that on input $n$, expressed
in base $4$, reaches a state with output $a(n)$. This Rudin-Shapiro automaton
is illustrated below in Figure 1. It is a simple variation on the one given in
[1].

Figure 1: DFAO computing the Rudin-Shapiro function, in base $4$.

Here states are labeled $a/b$, where $a$ is the state number and $b$ is the
output. The initial state is state $0$, and the automaton reads the digits of
the base-$4$ representation of $n$, starting with the most significant digit.
Leading zeros are allowed and do not affect the result.

Once the automaton in Figure 1 is saved as a file named RS4.txt, in Walnut we
can refer to its value at a variable $n$ simply by writing RS4[n]. We would
like to do the same thing for the Rudin-Shapiro summatory functions $s(n)$ and
$t(n)$ defined in Eqs. (1) and (2), but here we run into a fundamental
limitation of Walnut: it can only directly deal with functions of finite range
(like automatic sequences). Since $s(n)$ and $t(n)$ are unbounded, we must
find another way to deal with them.

A common way to handle functions in first-order logic is to treat them as
relations: instead of writing $f(n)=x$, we construct a relation $R_{f}(n,x)$
that is true iff $f(n)=x$. If the relation $R_{f}(n,x)$ is representable by a
deterministic finite automaton (DFA) taking as input $n$ in base $b_{1}$ and
$x$ in base $b_{2}$, in parallel, and accepting iff $R_{f}(n,x)$ holds, then
we say that $f$ is $(b_{1},b_{2})$-synchronized. For more information about
synchronized functions, see [6, 21].

Our first step, then, is to show that the functions $s(n)$ and $t(n)$ are
$(4,2)$-synchronized. These automata are illustrated in Figures 2 and 3. Here
accepting states are labeled by double circles.

Figure 2: Synchronized automaton for $s(n)$. Figure 3: Synchronized automaton
for $t(n)$.

We obtained these automata by “guessing” them from calculated initial values
of the sequences $s$ and $t$, using the Myhill-Nerode theorem [12, §3.4].
However, we will see below in Remark 4 that we could have also deduced them
from Satz 3 of [3] (Lemma 2 of [5]). The automaton for $s$ is called rss in
Walnut, and the automaton for $t$ is called rst.

Once we have guessed the automata, we need to verify they are correct.

######  Theorem 1.

The automata in Figs. (2) and (3) correctly compute $s(n)$ and $t(n)$.

###### Proof.

Let $s_{1}(n)$ (resp., $t_{1}(n)$) be the function computed by the automaton
in Fig. (2) (resp., Fig. (3)). We prove that $s_{1}(n)=s(n)$ and
$t_{1}(n)=t(n)$ by induction on $n$.

First we check that $s_{1}(0)=s(0)=1$ and $t_{1}(0)=t(0)=1$, which we can see
simply by inspecting the automata.

Now assume that $n\geq 1$ and $s_{1}(n)=s(n)$ and $t_{1}(n)=t(n)$. We prove
with Walnut that $s_{1}(n+1)=s_{1}(n)+a(n+1)$ and
$t_{1}(n+1)=t_{1}(n)+(-1)^{n+1}a(n+1)$.

    eval test1 "?msd_4 An,y ($rss(n,y) & RS4[n+1]=@1) => $rss(n+1,?msd_2 y+1)":
    eval test2 "?msd_4 An,y ($rss(n,y) & RS4[n+1]=@-1) => $rss(n+1,?msd_2 y-1)":
    # show that rss is correct

    def even4 "?msd_4 Ek n=2*k":
    def odd4 "?msd_4 Ek n=2*k+1":
    eval test3 "?msd_4 An,y ($rst(n,y) & ((RS4[n+1]=@1 & $even4(n+1)) |
       (RS4[n+1]=@-1 & $odd4(n+1)))) => $rst(n+1,?msd_2 y+1)":
    eval test4 "?msd_4 An,y ($rst(n,y) & ((RS4[n+1]=@-1 & $even4(n+1)) |
       (RS4[n+1]=@1 & $odd4(n+1)))) => $rst(n+1, ?msd_2 y-1)":
    # show that rst is correct

and Walnut returns TRUE for all of these tests. Now the correctness of our
automata follows immediately by induction. ∎

######  Remark 2.

Some Walnut syntax needs to be explained here. First, the capital A is Walnut’s abbreviation for $\forall$ (for all); capital E is Walnut’s abbreviation for $\exists$ (there exists); the jargon ?msd_$b$ for a base $b$ instructs that a parameter or expression is to be evaluated using base-$b$ numbers, and an @ sign indicates the value of an automatic sequence (which is allowed to be negative). The symbol & is logical AND; the symbol | is logical OR; and the symbol => is logical implication.

######  Remark 3.

There is a small technical wrinkle that we have glossed over, but it needs
saying: the default domain for Walnut is $\mathbb{N}$, the natural numbers.
But we do not know, a priori, that the functions $s$ and $t$ take only non-
negative values. Therefore, it is conceivable that our verification might fail
simply because negative numbers appear as intermediate values in a
calculation. We can check that this does not happen simply by checking that
rss and rst both are truly representations of functions:

    eval test5 "?msd_4 (An Ey $rss(n,y)) &
       An ~Ex,y ($rss(n,x) & $rss(n,y) & (?msd_2 x!=y))":
    eval test6 "?msd_4 (An Ey $rst(n,y)) &
       An ~Ex,y ($rst(n,x) & $rst(n,y) & (?msd_2 x!=y))":

These commands assert that for every $n$ there is at least one value $y$ such
that $s(n)=y$, and there are not two different such $y$, and the same for $t$.
Both evaluate to TRUE. This shows that the relations computed by rss and rst
are well-defined functions, and take only non-negative values. As a result, we
have already deduced Satz 11 of [3]: $t(n)\geq 0$ for all $n$.

The advantage of the representation of $s(n)$ and $t(n)$ as synchronized
automata is that they essentially encapsulate all the needed knowledge about
$s(n)$ and $t(n)$ to replace tedious inductions about them. The simple
induction we used to verify them replaces, in effect, all the other needed
inductions.

######  Remark 4.

The reader may reasonably ask, as one referee did, why use base-$4$ for $n$
and base-$2$ for the values of $s$ and $t$? The reason is because the values
of $s(n)$ and $t(n)$ grow like $\sqrt{n}$; if we are going to have any hope of
an automaton processing, say, $n$ and $s(n)$ in parallel, then length
considerations show that the base of representation for $n$ must be the square
of that for $s(n)$ and $t(n)$. Furthermore, by a classical theorem of Cobham
[7], the Rudin-Shapiro sequence itself can only be generated by an automaton
using base a power of $2$. This forces the base for $n$ to be $2^{2k}$ for
some $k$ and the base for $s$ and $t$ to be $2^{k}$.

All the code necessary to verify the results in this paper can be found at

https://cs.uwaterloo.ca/~shallit/papers.html .

##  4 Proofs of results

We can now begin to reprove, and in some cases, improve some of the results of
Brillhart and Morton. Let us start with their Satz 2 [3], reprised as Lemma 1
in [5]:

######  Theorem 5.

We have

$\displaystyle s(2n)$ $\displaystyle=s(n)+t(n-1),$ $\displaystyle\quad(n\geq
1);$ (3) $\displaystyle s(2n+1)$ $\displaystyle=s(n)+t(n),$
$\displaystyle\quad(n\geq 0);$ (4) $\displaystyle t(2n)$
$\displaystyle=s(n)-t(n-1),$ $\displaystyle\quad(n\geq 1);$ (5) $\displaystyle
t(2n+1)$ $\displaystyle=s(n)-t(n),$ $\displaystyle\quad(n\geq 0).$ (6)

###### Proof.

We use the following Walnut commands:

    eval eq3 "?msd_4 An,x,y,z (n>=1 & $rss(2*n,x) & $rss(n,y) & $rst(n-1,z))
       => ?msd_2 x=y+z":

    eval eq4 "?msd_4 An,x,y,z ($rss(2*n+1,x) & $rss(n,y) & $rst(n,z))
       => ?msd_2 x=y+z":

    eval eq5 "?msd_4 An,x,y,z (n>=1 & $rst(2*n,x) & $rss(n,y) & $rst(n-1,z))
       => ?msd_2 x+z=y":

    eval eq6 "?msd_4 An,x,y,z ($rst(2*n+1,x) & $rss(n,y) & $rst(n,z))
       => ?msd_2 x+z=y":

and Walnut returns TRUE for all of them.

For example, the Walnut formula eq3 asserts that for all $n,x,y,z$ if $n\geq
1$, $s(2n)=x$, $s(n)=y$, $t(n-1)=z$, then it must be the case that $x=y+z$. It
is easily seen that this is equivalent to the statement of Eq. (3).

Note that in our Walnut proofs of Eqs. (4) and (5), we rearranged the
statement to avoid subtractions. This is because Walnut’s basic domain is
$\mathbb{N}$, the natural numbers, and subtractions that could potentially
result in negative numbers might give anomalous results. ∎

We can now verify Satz 3 of [3] (Lemma 2 of [5]):

######  Lemma 6.

For $n\geq 0$ we have

$\displaystyle s(4n)$ $\displaystyle=2s(n)-a(n)$ (7) $\displaystyle s(4n+1)$
$\displaystyle=s(4n+3)=2s(n)$ (8) $\displaystyle s(4n+2)$
$\displaystyle=2s(n)+(-1)^{n}a(n).$ (9)

###### Proof.

We use the following Walnut commands:

    eval eq7 "?msd_4 An,x,y ($rss(4*n,x) & $rss(n,y)) =>
       ((RS4[n]=@1 => ?msd_2 x+1=2*y) & (RS4[n]=@-1 => ?msd_2 x=2*y+1))":

    eval eq8 "?msd_4 An,x,y,z ($rss(4*n+1,x) & $rss(4*n+3,y) & $rss(n,z))
       => ?msd_2 x=y & x=2*z":

    eval eq9 "?msd_4 An,x,y ($rss(4*n+2,x) & $rss(n,y)) =>
       (((RS4[n]=@1 & $even4(n)) => ?msd_2 x=2*y+1) &
       ((RS4[n]=@-1 & $even4(n)) => ?msd_2 x+1=2*y) &
       ((RS4[n]=@1 & $odd4(n)) => ?msd_2 x+1=2*y) &
       ((RS4[n]=@-1 & $odd4(n)) => ?msd_2 x=2*y+1))":

and Walnut returns TRUE for all of them. ∎

######  Remark 7.

As it turns out, Lemma 6 is more or less equivalent to our synchronized
automaton depicted in Figure 2. To see this, consider a synchronized automaton
where the first component represents $n$ in base $4$, while the second
component represents $s(n)$ in base $2$, but using the nonstandard digit set
$\\{-1,0,1\\}$ instead of $\\{0,1\\}$. Reading a bit $i$ in the first
component is like changing the number $n$ read so far into $4n+i$. Theorem 6
says that $s(4n+i)$ is twice $s(n)$, plus either $-1,0,$ or $1$, depending on
the value of $a(n)$ and the parity of $n$, both of which are (implicitly)
computed by the base-$4$ DFAO for $a(n)$. This gives us the automaton depicted
in Figure 4.

Figure 4: Synchronized automaton implementing Theorem 6. The state labels
record $a(n)$ and $n\bmod 2$.

To get the automaton in Figure 2 from this one, we would need to combine it
with a “normalizer” that can convert a nonstandard base-$2$ representation
into a standard one.

The sequence $t(n)$ satisfies a similar set of recurrences, which are given as
Satz 4 of [3].

######  Lemma 8.

We have

$\displaystyle t(4n)$ $\displaystyle=2t(n-1)+a(n),$ $\displaystyle\quad(n\geq
1);$ (10) $\displaystyle t(4n+1)$ $\displaystyle=2t(n-1),$
$\displaystyle\quad(n\geq 1);$ (11) $\displaystyle t(4n+2)$
$\displaystyle=t(n)+t(n-1),$ $\displaystyle\quad(n\geq 1);$ (12)
$\displaystyle t(4n+3)$ $\displaystyle=2t(n),$ $\displaystyle\quad(n\geq 0).$
(13)

###### Proof.

We use the following Walnut commands:

    eval eq10 "?msd_4 An,x,y (n>=1 & $rst(4*n,x) & $rst(n-1,y)) =>
       ((RS4[n]=@1 => ?msd_2 x=2*y+1) & (RS4[n]=@-1 => ?msd_2 x+1=2*y))":

    eval eq11 "?msd_4 An,x,y (n>=1 & $rst(?msd_4 4*n+1,x) &
       $rst(?msd_4 n-1,y)) => ?msd_2 x=2*y":

    eval eq12 "?msd_4 An,x,y,z (n>=1 & $rst(4*n+2,x) &
       $rst(n,y) & $rst(n-1,z)) => ?msd_2 x=y+z":

    eval eq13 "?msd_4 An,x,y ($rst(4*n+3,x) & $rst(n,y)) => ?msd_2 x=2*y":

and Walnut returns TRUE for all of them. ∎

Next we give Theorem 1 of [5].

######  Theorem 9.

  * (a)

For $k\geq 1$, the minimum value of $s(n)$ for $n\in[4^{k},4^{k+1}-1]$ is
$2^{k}+1$ and $s(n)$ attains this value only when $n=4^{k}$ or $n=(5\cdot
4^{k}-2)/3$.

  * (b)

For $k\geq 0$, the maximum value of $s(n)$ for $n\in[4^{k},4^{k+1}-1]$ is
$2^{k+2}-1$ and $s(n)$ attains this value only when
$n=M_{k}:=\frac{2}{3}(2^{2k+2}-1)$.

###### Proof.

We use the following Walnut commands:

    reg rss_int msd_4 msd_4 "[0,0]*[1,3][0,3]*":

    eval min_rss "?msd_4 n>=4 & $rss(n, x) & Ei,j $rss_int(i,j) &
       i<=n & n<=j & (Ay,m (i<=m & m<=j & $rss(m,y)) =>
       ?msd_2 y>=x)":

    eval max_rss "?msd_4 $rss(n, x) & Ei,j $rss_int(i,j) &
       i<=n & n<=j & (Ay,m (i<=m & m<=j & $rss(m,y)) =>
       ?msd_2 y<=x)":

The output of these commands is the automata displayed in Figures 5 and 6. The
automata accept pairs $((n)_{4},(s(n))_{2})$ where $s(n)$ is extremal for $n$
in the specified interval. The first automaton accepts
$[0,0]^{*}[1,1][0,0]^{*}[0,1]$ and $[0,0]^{*}[1,1][2,0]^{*}[2,1]$ and the
second automaton accepts $[0,0]^{*}[0,1][2,1][2,1]^{*}$. From this one easily
deduces the result. ∎

Figure 5: Automaton for the minimum value of $s(n)$, $n\in[4^{k},4^{k+1}-1]$.
Figure 6: Automaton for the maximum value of $s(n)$, $n\in[4^{k},4^{k+1}-1]$.

###  4.1 The $\omega$ function

Brillhart and Morton defined a function, $\omega(k)$, as follows: $\omega(k)$
is the largest value of $n$ for which $s(n)=k$. This is sequence A020991 in
the OEIS. We can create a $(2,4)$-synchronized automaton for $\omega$ as
follows:

    def omega "?msd_4 $rss(n,k) & At (t>n) => ~$rss(t,k)":

We can then create a $(2,4)$-synchronized automaton for
$\omega(n+1)-\omega(n)$ as follows:

    def omegadiff "?msd_4 Et,u $omega((?msd_2 n+1),t) &
       $omega(n,u) & t=x+u":

Let us now show that $\omega(s(n))\leq(10n-2)/3$ for $n\geq 2$.

    def omegas "?msd_4 Ek $rss(n,k) & $omega(k,x)":
    eval check_bounds "?msd_4 An,t (n>=2 & $omegas(n,t)) => 3*t+2<=10*n":

Also this bound is optimal, because it holds for $n=2^{2i+1}$ and $i\geq 0$.

Now let us prove Lemma 5 of Brillhart and Morton [5].

######  Theorem 10.

We have

$\displaystyle\omega(2n)$ $\displaystyle=4\omega(n)+3,$ $\displaystyle\quad
n\geq 1;$ (14) $\displaystyle\omega(2n+1)$ $\displaystyle=4\omega(n+1)+2,$
$\displaystyle\quad n\geq 2,\ n+1\not=2^{r},\ r\geq 2.$ (15)

###### Proof.

Let us prove Eq. (14).

    eval eq14 "?msd_4 An,x,y ((?msd_2 n>=1) & $omega(n,x) &
       $omega((?msd_2 2*n), y)) => y=4*x+3":

Brillhart and Morton claim that the proof of the second equality is “much
trickier”. However, with Walnut it is not really much more difficult than the
previous one.

    reg power2 msd_2 "0*10*":
    eval eq15 "?msd_4 An,x,y (?msd_2 n>=2 & (~$power2(?msd_2 n+1)) &
       $omega((?msd_2 n+1),x) & $omega((?msd_2 2*n+1),y)) => y=4*x+2":

∎

##  5 More lemmas

Let us now prove Lemma 3 of [5]:

######  Theorem 11.

We have

$\displaystyle s(n+2^{2k})$ $\displaystyle=s(n)+2^{k},$ $\displaystyle\quad
0\leq n\leq 2^{2k-1}-1,\ k\geq 1;$ (16) $\displaystyle s(n+2^{2k})$
$\displaystyle=-s(n)+3\cdot 2^{k},$ $\displaystyle\quad 2^{2k-1}\leq n\leq
2^{2k}-1,\ k\geq 1;$ (17) $\displaystyle s(n+2^{2k+1})$
$\displaystyle=s(n)+2^{k+1},$ $\displaystyle\quad 0\leq n\leq 2^{2k}-1,\ k\geq
0;$ (18) $\displaystyle s(n+2^{2k+1})$ $\displaystyle=-s(n)+2^{k+2},$
$\displaystyle\quad 2^{2k}\leq n\leq 2^{2k+1}-1,\ k\geq 0.$ (19)

###### Proof.

We can prove these identities with Walnut. One small technical difficulty is
that the equation $x=2^{n}$ is not possible to express in the particular
first-order logic that Walnut is built on; it cannot even multiply arbitrary
variables, or raise a number to a power. Instead, we assert that $x$ is a
power of $2$ without exactly specifying which power of $2$ it is. This brings
up a further difficulty, which is that we need to simultaneously express
$2^{2k}$ and $2^{k}$. Normally this would also not be possible in Walnut.
However, in this case the former is expressed in base $4$ and the latter in
base $2$, we can achieve this using the link42 automaton:

    reg power4 msd_4 "0*10*":
    reg link42 msd_4 msd_2 "([0,0]|[1,1])*":

Here power4 asserts that its argument is a power of $4$; specifically, that
its base-$4$ representation looks like $1$ followed by some number of $0$’s,
and also allowing any number of leading zeros. If this is true for $x$, then
$x=4^{k}$ for some $k$, and link42 applied to the pair $(x,y)$ asserts that
$y=2^{k}$ (by asserting that the base-$4$ representation $x$ is the same as
the base-$2$ representation of $y$).

To verify Eqs. (16)–(19), we use the following Walnut code:

    eval eq16 "?msd_4 An,x,y,z ($power4(x) & x>=4 & 2*n+2<=x &
       $rss(n,y) & $link42(x,z)) => $rss(n+x,?msd_2 y+z)":
    eval eq17 "?msd_4 An,x,y,z ($power4(x) & x>=4 & 2*n>=x & n<x & $rss(n,y)
       & $link42(x,z)) => $rss(n+x,?msd_2 3*z-y)":
    eval eq18 "?msd_4 An,x,y,z ($power4(x) & n<x & $rss(n,y) & $link42(x,z))
       => $rss(n+2*x,?msd_2 y+2*z)":
    eval eq19 "?msd_4 An,x,y,z ($power4(x) & x<=n & n<2*x & $rss(n,y) &
       $link42(x,z)) => $rss(n+2*x,?msd_2 4*z-y)":

∎

We now turn to Lemma 4 in Brillhart and Morton [5]. It is as follows (where we
have corrected a typographical error in the original statement).

######  Theorem 12.

Suppose $n\in[2^{2k},2^{2k+1})$. Then $s(n)\leq 2^{k+1}$, and furthermore,
equality holds for $n$ in this range iff $n=2^{2k+1}-1-\sum_{0\leq
r<k}e_{r}2^{2r+1},$ where the $e_{r}\in\\{0,1\\}$.

###### Proof.

We can verify the first claim as follows:

     eval lemma4 "?msd_4 An,x,y,z ($power4(x) & x<=n & n<2*x &
        $link42(x,z) & $rss(n,y)) => ?msd_2 y<=2*z":

For the second, let us create a synchronized automaton accepting the base-$4$
representation of $k$ and $n$ for which $s(n)=2^{k+1}$.

     def lemma4a "?msd_4 Ez $power4(x) & x<=n & n<2*x &
        $link42(x,z) & $rss(n,?msd_2 2*z)":

By examining the result, we see that the only accepted paths are labeled with
$[1,1]\\{[1,0],[3,0]\\}^{*}$. This is easily seen to be the same as the claim
in the Brillhart-Morton result. ∎

##  6 Special values

Along the way, Brillhart and Morton proved a large number of results about
special values of the functions $s$ and $t$. These are very easily proved with
Walnut.

Let us start with Examples (“Beispiel”) 5–10 of [3].

######  Theorem 13.

We have

  * (a)

$s(2^{k})=2^{\lfloor(k+1)/2\rfloor}+1$ for $k\geq 0$;

  * (b)

$s(2^{k}-1)=2^{\lfloor(k+1)/2\rfloor}$ for $k\geq 0$;

  * (c)

$s(2^{k}-2)=2^{\lfloor(k+1)/2\rfloor}+(-1)^{k}$ for $k\geq 1$;

  * (d)

$s(3\cdot 2^{2k}-1)=3\cdot 2^{k}$ for $k\geq 0$;

  * (e)

$s(3\cdot 2^{2k+1}-1)=2^{k+2}$ for $k\geq 0$;

  * (f)

$t(2^{2k})=2^{k}+1$ for $k\geq 1$;

  * (g)

$t(2^{2k+1})=1$ for $k\geq 0$;

  * (h)

$t(2^{2k}-1)=2^{k}$ for $k\geq 0$;

  * (i)

$t(2^{2k+1}-1)=0$ for $k\geq 0$;

  * (j)

$t(2^{2k}-2)=2^{k}-1$ for $k\geq 1$;

  * (k)

$t(2^{2k+1}-2)=1$ for $k\geq 0$;

  * (l)

$t(3\cdot 2^{k}-1)=2^{\lfloor(k+1)/2\rfloor}$ for $k\geq 0$.

###### Proof.

We can verify all of these by straightforward translation of the assertions
into Walnut. First let’s write a formula asserting $x=2^{k}$ and
$y=2^{\lfloor(k+1)/2\rfloor}$, where the former is expressed in base $4$ and
the latter in base $2$.

    reg sqrtpow2 msd_4 msd_2 "[0,0]*([1,1]|[0,1][2,0])[0,0]*":

Then we can verify all the assertions as follows:

    reg oddpow2 msd_4 "0*20*":
    eval specval_a "?msd_4 Ax,y $sqrtpow2(x,y) => $rss(x,?msd_2 y+1)":
    eval specval_b "?msd_4 Ax,y $sqrtpow2(x,y) => $rss(x-1,?msd_2 y)":
    eval specval_c1 "?msd_4 Ax,y ($power4(x) & x>1 & $sqrtpow2(x,y))
       => $rss(x-2, ?msd_2 y+1)":
    eval specval_c2 "?msd_4 Ax,y ($oddpow2(x) & $sqrtpow2(x,y))
       => $rss(x-2, ?msd_2 y-1)":
    eval specval_d "?msd_4 Ax,y ($power4(x) & $link42(x,y))
       => $rss(3*x-1,?msd_2 3*y)":
    eval specval_e "?msd_4 Ax,y ($oddpow2(x) & $sqrtpow2(x,y))
       => $rss(3*x-1,?msd_2 2*y)":
    eval specval_f "?msd_4 Ax,y ($power4(x) & x>1 & $link42(x,y))
       => $rst(x,?msd_2 y+1)":
    eval specval_g "?msd_4 Ax $oddpow2(x) => $rst(x,?msd_2 1)":
    eval specval_h "?msd_4 Ax,y ($power4(x) & $link42(x,y))
       => $rst(x-1,?msd_2 y)":
    eval specval_i "?msd_4 Ax $oddpow2(x) => $rst(x-1,?msd_2 0)":
    eval specval_j "?msd_4 Ax,y ($power4(x) & x>1 & $link42(x,y))
       => $rst(x-2, ?msd_2 y-1)":
    eval specval_k "?msd_4 Ax $oddpow2(x) => $rst(x-2,?msd_2 1)":
    eval specval_l "?msd_4 Ax,y $sqrtpow2(x,y) => $rst(3*x-1,y)":

∎

Satz 10 of [3] gives the values of $n$ for which $t(n)=0$. We can find these
with the Walnut command

    def satz10 "$rst(?msd_4 n,?msd_2 0)":

The resulting automaton appears in Figure 7.

Figure 7: DFA accepting those $n$ for which $t(n)=0$, expressed in base $4$.

Examining this automaton gives the following:

######  Theorem 14.

We have $t(n)=0$ iff $(n)_{4}\in 13^{*}\,\cup\,2\\{0,2\\}^{*}13^{*}$.

Next let us determine those $n$ for which $s(n)=t(n)$. We can define the
base-$4$ representation of such $n$ with the following Walnut command:

    def same "Ex $rss(n,x) & $rst(n,x)":

The resulting automaton appears in Figure 8.

Figure 8: DFA accepting those $n$ for which $s(n)=t(n)$, expressed in base
$4$.

We have therefore proved the following result, which is given as a Zusatz to
Satz 10 of [3].

######  Theorem 15.

We have $s(n)=t(n)$ if and only if $n=0$ or $(n)_{4}\in
3^{*}\,\cup\,1\\{0,1\\}^{*}\,0\,3^{*}$.

From Theorem 14 we see that the minimum value of $t(n)$ is $0$ and $t(n)$
takes this value infinitely often. The next result, which is an analogue of
Theorem 9 (Satz 12 of [3]), gives the maximum value of $t(n)$ on certain
intervals.

######  Theorem 16.

  * (a)

For $k\geq 1$, the maximum value of $t(n)$ for $n\in[4^{k},2\cdot 4^{k}-1]$ is
$2^{k+1}-1$ and $t(n)$ attains this value only when $n=4(2^{2k}-1)/3$.

  * (b)

For $k\geq 1$, the maximum value of $t(n)$ for $n\in[2\cdot 4^{k},4^{k+1}-1]$
is $2^{k+1}$ and $t(n)$ attains this value only when $n=2^{2k+2}-1$.

###### Proof.

We use the following Walnut commands:

    reg rst_int1 msd_4 msd_4 "[0,0]*[1,1][0,3]*":
    reg rst_int2 msd_4 msd_4 "[0,0]*[2,3][0,3]*":

    eval max_rst1 "?msd_4 n>=2 & $rst(n, ?msd_2 x) & Ei,j $rst_int1(i,j) &
    i<=n & n<=j & (Ay,m (i<=m & m<=j & $rst(m,?msd_2 y)) => ?msd_2 y<=x)":

    eval max_rst2 "?msd_4 n>=4 & $rst(n, ?msd_2 x) & Ei,j $rst_int2(i,j) &
    i<=n & n<=j & (Ay,m (i<=m & m<=j & $rst(m,?msd_2 y)) => ?msd_2 y<=x)":

The output of these commands is the automata displayed in Figures 9 and 10.
The automata accept pairs $((n)_{4},(t(n))_{2})$ where $t(n)$ is extremal for
$n$ in the specified interval. The first automaton accepts
$[0,0]^{*}[1,1][1,1]^{*}[0,1]$ and the second automaton accepts
$[0,0]^{*}[3,0][3,0][3,0]^{*}$. From this one easily deduces the result. ∎

Figure 9: Automaton for the maximum value of $t(n)$, $n\in[4^{k},2\cdot
4^{k}-1]$. Figure 10: Automaton for the maximum value of $t(n)$, $n\in[2\cdot
4^{k},4^{k+1}-1]$.

Let us now prove Satz 14 of [3]:

######  Theorem 17.

We have

  * (a1)

$s(4(2^{2k}-1)/3)=2^{k+1}-1$ for $k\geq 0$;

  * (a2)

$s(2^{2k+2}-1)=2^{k+1}$ for $k\geq 0$;

  * (b1)

$t(2^{2k})=2^{k}+1$ for $k\geq 1$;

  * (b2)

$t((5\cdot 2^{2k}-2)/3)=2^{k}-1$ for $k\geq 0$;

  * (c)

If $0\leq s<2^{k}$ then $t(2^{2k+1}-1-2m(s))=2s$;

  * (d)

If $0\leq s<2^{k}$ then $t(2^{2k+2}-1-2m(s))=2^{k+1}-2s$;

  * (e)

$t(2(2^{2k+2}-1)/3)=1$ for $k\geq 0$.

###### Proof.

The following straightforward translations of the assertions all evaluate to
TRUE in Walnut:

    eval eq24a1 "?msd_4 An,x,y,z ($power4(x) & $link42(x,y) & 3*n+4=4*x &
       $rss(n,z)) => ?msd_2 z+1=2*y":
    eval eq24a2 "?msd_4 An,x,y,z ($power4(x) & $link42(x,y) & n+1=4*x &
       $rss(n,z)) => ?msd_2 z=2*y":
    eval eq24b1 "?msd_4 Ax,y,z ($power4(x) & x>1 & $link42(x,y) & $rst(x,z))
       => ?msd_2 z=y+1":
    eval eq24b2 "?msd_4 An,x,y,z ($power4(x) & $link42(x,y) & 3*n+2=5*x &
       $rst(n,z)) => ?msd_2 z+1=y":
    eval eq24c "?msd_4 An,s,x,y,w,z ($power4(x) & $link42(x,w) & $link42(y,s)
       & (?msd_2 s<w) & n+2*y+1=2*x & $rst(n,z)) => ?msd_2 z=2*s":
    eval eq24d "?msd_4 An,s,x,y,w,z ($power4(x) & $link42(x,w) & $link42(y,s)
       & (?msd_2 s<w) & n+2*y+1=4*x & $rst(n,z)) => ?msd_2 z+2*s=2*w":
    eval eq24e "?msd_4 Ax,n ($power4(x) & 3*n+2=8*x) => $rst(n,?msd_2 1)":

∎

##  7 Inequalities

We showed in Theorem 1 that $s(n)$ and $t(n)$ are $(4,2)$-synchronized;
furthermore, $s(n)$ and $t(n)$ are both unbounded as is easily verified with
Walnut. A basic result about synchronized sequences, namely Theorem 8 of [21],
immediately implies that there are constants $c^{\prime}$ and
$c^{\prime\prime}$ such that $c^{\prime}\leq s(n)/\sqrt{n}\leq
c^{\prime\prime}$, and similarly for $t(n)$. The main accomplishment of
Brillhart and Morton’s paper was to determine these constants.

######  Theorem 18 (Brillhart & Morton).

For $n\geq 1$ we have

$\displaystyle\sqrt{3n/5}$ $\displaystyle\leq s(n)\leq\sqrt{6n}$
$\displaystyle 0$ $\displaystyle\leq t(n)\leq\sqrt{3n}.$

Trying to prove these results by directly translating the claims into Walnut
leads to two difficulties: first, automata cannot compute squares or square
roots. Second, our synchronized automata work with $n$ expressed in base $4$,
but $s(n)$ and $t(n)$ are expressed in base $2$, and Walnut cannot directly
compare arbitrary integers expressed in different bases.

However, there is a way around both of these difficulties. First, we define a
kind of “pseudo-square” function as follows: $m(n)=[(n)_{2}]_{4}$. In other
words, $m$ sends $n$ to the integer obtained by interpreting the base-$2$
expansion of $n$ as a number in base $4$. Luckily we have already defined an
automaton for $m$ called link42; to get an automaton for $m$, we only have to
reverse the order of the arguments in link42!

Now we need to see how far away from a real squaring function our pseudo-
square function $m(n)$ is.

######  Lemma 19.

We have $(n^{2}+2n)/3\leq m(n)\leq n^{2}$.

###### Proof.

We can prove the bounds by induction on $n$. They are clearly true for $n=0$.
Assume $n\geq 1$ and the inequalities hold for all $n^{\prime}<n$; we prove
them for $n$.

Suppose $n$ is even. Then $n=2k$. Clearly $m(n)=4m(k)$. By induction we have
$(k^{2}+2k)/3\leq m(k)\leq k^{2}$, and multiplying through by $4$ gives

$(n^{2}+2n)/3=(4k^{2}+4k)/3<4(k^{2}+2k)/3\leq 4m(k)\leq 4k^{2}=n^{2}.$

Suppose $n$ is odd. Then $n=2k+1$. Clearly $m(n)=4m(k)+1$. By induction we
have $(k^{2}+2k)/3\leq m(k)\leq k^{2}$. Multiplying by $4$ and adding $1$
gives

$(n^{2}+2n)/3=((2k+1)^{2}+2(2k+1))/3=(4k^{2}+8k+3)/3\leq 4m(k)+1\leq
4k^{2}+1\leq(2k+1)^{2}=n^{2},$

as desired. ∎

We can now prove:

######  Lemma 20.

For $n\geq 1$ we have ${{3n+7}\over 5}\leq m(s(n))\leq 3n+1$, and the upper
and lower bounds are tight.

###### Proof.

We use the Walnut code

    def maps "?msd_4 Ex $rss(n,x) & $link42(y,x)":
    eval ms_lowerbnd "?msd_4 An,y (n>=1 & $maps(n,y)) => y<=3*n+1":
    eval ms_upperbnd "?msd_4 An,y (n>=1 & $maps(n,y)) => 3*n+7<=5*y":

To show they are tight, let us show there are infinitely many solutions to
$m(s(n))=3n+1$ and $m(s(n))=(3n+7)/5$:

    eval lowerbnd_tight "?msd_4 Am En,y (n>m) & $maps(n,y) & y=3*n+1":
    eval upperbnd_tight "?msd_4 Am En,y (n>m) & $maps(n,y) & 5*y=3*n+7":

∎

As a consequence, we get one lower bound in Theorem 18.

######  Corollary 21.

For $n\geq 1$ we have

$s(n)\geq\sqrt{{3n+7}\over 5}.$

###### Proof.

From Theorem 19 we have $m(s(n))\leq s(n)^{2}$ and from Lemma 20 we have
${{3n+7}\over 5}\leq m(s(n))$. Putting these two bounds together gives
${{3n+7}\over 5}\leq s(n)^{2}$. ∎

Note that our lower bound is actually slightly stronger than that of
Brillhart-Morton!

To get the upper bound $s(n)\leq\sqrt{6n}$, as in Brillhart-Morton, we need to
do more work, since the results we have proved so far only suffice to show
that $s(n)\leq\sqrt{9n+3}$. To get their upper bound, Brillhart and Morton
carved the various intervals for $n$ up into three classes and proved the
upper bound of $\sqrt{6n}$ for each class. We’ll do the same thing, but use
slightly different classes. By doing so we avoid their complicated induction
entirely.

The first class is the easiest: those $n$ for which $m(s(n))\leq 2n$. For
these $n$, Lemma 19 immediately gives us $s(n)^{2}\leq 6n$, as desired.
Furthermore, the “exceptional set” (that is, those $n$ for which $m(s(n))>2n$)
is calculatable with Walnut:

    def exceptional_set "?msd_4 Em $maps(n,m) & m>2*n":

The resulting automaton is quite simple (2 states!) and recognizes the set of
base-$4$ expansions $\\{0,2\\}^{*}\,\cup\,\\{0,2\\}^{*}\ 1\ \\{1,3\\}^{*}$.

We readily see, then, that the exceptional set consists of

  * (a)

numbers whose base-$4$ expansion starts with a $1$ and thereafter consists of
$1$’s and $3$’s, and

  * (b)

the rest, which must start with a $2$.

The numbers in group (a) are easiest to deal with, because they satisfy the
inequality $M_{k}/2\leq n<2^{2k+1}$ for some $k\geq 0$. (Recall that
$M_{k}=(2^{2k+3}-2)/3$ was defined in Theorem 9.) Now for all $n$ (not just
those in the exceptional set) in the half-open interval $I_{k}:=[M_{k}/2,\
2^{2k+1})$ we can show with Walnut that $s(n)\leq 2^{k+1}$, as follows:

    eval maxcheck "?msd_4 An,x,y,z ($power4(x) & 3*n+1>=4*x & n<2*x
       & $rss(n,y) & $link42(x,z)) => ?msd_2 y<=2*z":

So for all $n\in I_{k}$ we have

${{s(n)^{2}}\over{n}}\leq{(\max_{n\in I_{k}}s(n))^{2}\over{\min_{n\in
I_{k}}n}}={{(2^{k+1})^{2}}\over{M_{k}/2}}=3{{2^{2k+2}}\over{2^{2k+2}-1}}\leq
4.$

This handles the numbers in group (a).

Finally, we turn to group (b), which are the hardest to deal with. These
numbers lie in the interval $I^{\prime}_{k}=[2^{2k+1},M_{k}]$. We will split
these numbers into the following intervals:
$J_{k,i}:=[M_{k}-M_{i},M_{k}-M_{i-1})$ for $0\leq i<k$. Since
$M_{k}-M_{k-1}=2^{2k+1}$, the union

$J_{k,0}\,\cup\,J_{k,1}\,\cup\,\cdots\,\cup\,J_{k,k-1}\,\cup\,\\{M_{k}\\}$

forms a disjoint partition of the interval $I^{\prime}_{k}$.

Now with Walnut we can prove that for $n\in J_{k,i}$ we have $s(n)\leq
2^{k+2}-2^{i+1}$.

    eval J_inequality "?msd_4 An,x,y,z,w,m ($rss(n,m) & $power4(x) & $power4(y)
       & x>y & $link42(x,w) & $link42(y,z) & 8*x<=3*n+8*y & 3*n+2*y<8*x)
       => ?msd_2 m+2*z<=4*w":

It now follows that for $n\in J_{k,i}$, $k\geq 1$, and $0\leq i<k$, we have

${{s(n)^{2}}\over{n}}\leq{{(\max_{n\in J_{k,i}}s(n))^{2}}\over{\min_{n\in
J_{k,i}}n}}\leq{{(2^{k+2}-2^{i+1})^{2}}\over{M_{k}-M_{i}}}$

and a routine manipulation666Here are the details. Since $k\geq 1$ and $0\leq
i<k$ we clearly have $2^{k+2}>5\cdot 2^{i}=2^{i+2}+2^{i}$. Multiplying by
$2^{i+2}$ gives us $2^{k+i+4}>2^{2i+4}+2^{2i+2}$. Adding $2^{2k+4}$ to both
sides, and rearranging gives $2^{2k+4}-2^{k+i+4}+2^{2i+2}<2^{2k+4}-2^{2i+4}$.
In other words, $(2^{k+2}-2^{i+1})^{2}<2(2^{2k+3}-2^{2i+3})$. Hence
$(2^{k+2}-2^{i+1})^{2}/(2^{2k+3}-2^{2i+3})<2$, and so
$(2^{k+2}-2^{i+1})^{2}/(M_{k}-M_{i})<6$. shows this is less than $6$.

The only remaining case is $M_{k}$. But then $s(M_{k})=2^{k+2}-1$, and then
$s(M_{k})^{2}<6M_{k}$ by another routine calculation.

Finally, we should verify that we have really covered all the possible $n$:

    def left_endpoint "?msd_4 3*z+8*y=8*x":
    def right_endpoint "?msd_4 3*z+2*y=8*x":
    eval check_all "?msd_4 An (n>=1) => ((~$exceptional_set(n)) |
       (Ex $power4(x) & 4*x<=3*n+1 & n<2*x) |
       (Ex,y,z,w $power4(x) & $power4(y) & x>y &
       $left_endpoint(x,y,z) & $right_endpoint(x,y,w) & n>=z & n<w) |
       (Ex $power4(x) & 3*n+2=8*x))":

which evaluates to TRUE.

Thus we have proved one upper bound from Theorem 18:

######  Theorem 22.

$s(n)\leq\sqrt{6n}$ for $n\geq 1$.

Using exactly the same techniques we can prove

######  Lemma 23.

For all $n\geq 0$ we have $m(t(n))\leq n+1$, with equality iff
$(n)_{4}\in(0\,\cup\,11^{*}0)^{*}3^{*}$.

###### Proof.

We use the following Walnut code:

    def mapt "?msd_4 Ex $rst(n,x) & $link42(y,x)":
    eval bnd "?msd_4 An,z $mapt(n,z) => z<=n+1":
    def except2 "?msd_4 Ez $mapt(n,z) & z=n+1":

The command bnd returns TRUE, and the command except2 computes a simple
automaton of 3 states accepting the regular expression
$(0\,\cup\,11^{*}0)^{*}3^{*}$. ∎

From the first claim of Lemma 23 we see that $m(t(n))\leq n+1$, and by Lemma
19 we have $t(n)^{2}/3\leq m(t(n))$. Putting these bounds together gives us
$t(n)\leq\sqrt{3(n+1)}$, which is very close to the Brillhart-Morton upper
bound for $t(n)$.

To get the other Brillhart-Morton upper bound of Theorem 18, we just use Eqs.
(3) and (4), just as Brillhart and Morton did. This gives us

$t(n)=s(n/2)-t(n/2-1)\leq s(n/2)\leq\sqrt{3n}$

for $n\geq 2$ even and

$t(n)=s((n-1)/2)-t((n-1)/2)\leq s((n-1)/2)\leq\sqrt{3(n-1)}$

for $n$ odd. Thus we have proved

######  Theorem 24.

We have $t(n)\leq\sqrt{3n}$ for $n\geq 1$.

We can also reprove, in an extremely simple fashion, an inequality of
Brillhart and Morton on the $\omega$ function introduced previously. Let us
start by showing

######  Lemma 25.

For $k\geq 0$ we have $\omega(k)\leq{5\over 3}m(k)$.

###### Proof.

We verify this with the following Walnut command.

    eval omegabound "?msd_4 Ak,x,y ($omega(k,x) & $link42(y,k)) => 3*x<=5*y":

and it returns TRUE. ∎

This, combined with Lemma 19 gives a proof of Theorem 5 in Brillhart and
Morton [5]:

######  Corollary 26.

We have $\omega(k)\leq{5\over 3}k^{2}$ for $k\geq 0$.

##  8 Counting the $k$ for which $s(k)=n$

One of the most fun properties of the Rudin-Shapiro summation function $s(n)$
is Satz 22 of [3]:

######  Theorem 27.

There are exactly $n$ values of $k$ for which $s(k)=n$.

###### Proof.

We can prove this theorem “purely mechanically” by using another capability of
Walnut: the fact that it can create base-$b$ linear representations for values
of synchronized sequences. By a base-$b$ linear representation for a function
$f(n)$ we mean vectors $v,w$, and a matrix-valued morphism $\gamma$ such that
$f(n)=v\gamma(x)w$ for all strings $x$ representing $n$ in base $b$. The rank
of a linear representation is the dimension of $v$.

So let us find a base-$2$ linear representation for the number of such $k$ for
which $s(k)=n$:

    eval satz22 n "$rss(?msd_4 k,n)":

This gives us a base-$2$ linear representation of rank $7$ computing some
function $f(n)$. Next we use Walnut to compute a base-$2$ linear
representation for the function $g(n)=n$:

    eval gfunc n "i<n":

From this, we can easily compute a base-$2$ linear representation for
$f(n)-g(n)$, and minimize it using an algorithm777Maple code implementing this
algorithm is available from the second author. of Schützenberger [2, §2.3].
When we do so, we get the representation for the $0$ function, so $f(n)=n$. ∎

##  9 New results

One big advantage to the synchronized representation of the Rudin-Shapiro sum
functions is that it becomes almost trivial to explore and rigorously prove
new properties. As a new result, let’s consider the analogue of Theorem 27,
but for the function $t$. Here we run into the problem that every natural
number $k$ appears as a value of $t(n)$ infinitely often:

    eval tvalues "?msd_4 An,k Em (m>n) & $rst(m,k)":

and Walnut returns TRUE.

So it makes sense to count the number of times $k$ appears as a value of
$t(n)$ in some initial segment, say the first $0,1,\ldots,2^{r}-1$.

Some empirical calculations suggest the following conjecture:

######  Theorem 28.

  * (a)

For $n\in[0,4^{m}/2)$, $0$ appears as a value of $t(n)$ exactly $2^{m-1}$
times, and $k$ appears exactly $2^{m}-k$ times for $1\leq k<2^{m}$.

  * (b)

For $n\in[0,4^{m})$, $0$ appears as a value of $t(n)$ exactly $2^{m}-1$ times,
$2^{m}$ appears exactly once, and $k$ appears $2(2^{m}-k)$ times for $1\leq
k<2^{m}$.

###### Proof.

We use the following Walnut commands.

    def counta1 k x "?msd_4 $rst(n,k) & $power4(x) & x>1 & 2*n<x ":

    def counta2 k x "?msd_4 Ey $power4(x) & x>1 & $link42(x,y) &
       (?msd_2 (k=0 & 2*n<y)|(1<=k & k<y & n+k<y))":

    def countb1 k x "?msd_4 $rst(n,k) & $power4(x) & n<x":

    def countb2 k x "?msd_4 Ey $power4(x) & $link42(x,y) &
       (?msd_2 (k=0 & n+1<y)|(k=y & n=0)|(1<=k & k<y & n+2*k<2*y))":

The first two statements are used for part (a). The code counta1 asserts that
$x=4^{m}$ for some $m$, and that $t(n)=k$ for some $n<x$. It returns a linear
representation for the number of $n$ for which this holds, as a function of
$k$ and $x$. The code counta2 creates a formula that says that the number of
$n$ fulfills the conclusion of the theorem. From these linear representations
we can create a linear representation for their difference. When we minimize
it, we get the linear representation for the $0$ function, so they compute the
same function.

The same approach is used for (b). ∎

###  9.1 The $\alpha$ function

We now introduce an analogue of Brillhart and Morton’s $\omega$ function, but
for the first occurrence of each distinct value of $s(n)$; i.e., we define
$\alpha(k)$ to be the smallest value of $n$ for which $s(n)=k$. We can create
a $(2,4)$-synchronized automaton for $\alpha$ as follows:

    def alpha "?msd_4 $rss(n,k) & At (t<n) => ~$rss(t,k)":

This automaton is given in Figure 11.

Figure 11: $(2,4)$-synchronized automaton for $\alpha$.

######  Theorem 29.

Let $k\geq 1$ and write $k=k^{\prime}2^{\ell}$ where $k^{\prime}$ is odd. Then

$\alpha(k)=m(k)/2-(2\cdot 4^{\ell-1}+1)/3.$

###### Proof.

Let $(k,n)$ be a pair accepted by the automaton in Figure 11. Suppose
$\ell\geq 2$. Note that $(k)_{2}$ ends with $\ell$ $0$’s and $(n)_{4}$ ends
with $\ell$ $1$’s. Let $r=[2^{\ell-2}3]_{4}$. We observe that $(4(n+r))_{4}$
consists only of $0$’s and $2$’s and has $2$’s exactly where $(k)_{2}$ has
$1$’s. It follows that $4(n+r)=2m(k)$; i.e.,

$4\left(n+2\sum_{i=0}^{\ell-2}4^{i}+1\right)=2m(k),$

which gives $\alpha(k)=n=m(k)/2-(2\cdot 4^{\ell-1}+1)/3$, as required. The
cases $\ell=0,1$ are similar. ∎

Similarly, we can consider the analogue of the $\alpha$ function for $t$
instead of $s$; let us call it $\alpha^{\prime}$. Remarkably,
$\alpha^{\prime}$ has a very simple expression in terms of known functions:

######  Theorem 30.

Define $\alpha^{\prime}(k)=\min\\{n\,:\,t(n)=k\\}$. Then
$\alpha^{\prime}(k)=m(k)-1$ for all $k\geq 1$.

###### Proof.

We use the following Walnut code:

    def alphap "?msd_4 $rst(n,k) & At (t<n) => ~$rst(t,k)":
    eval verify_alphap "?msd_4 Ak,t ((?msd_2 k>=1) & $alphap(k,t)) =>
       $link42(t+1,k)":

and Walnut returns TRUE. ∎

##  10 Plane-filling curves

In this section we show how to use our automata to prove results about the
space-filling curve generated by connecting the lattice points $P_{n}$ in the
plane defined by $P_{n}=(x(n),y(n))$ for $n\geq 0$. This curve was previously
explored in the papers [18, 17, 9]. The first $1024$ points of this curve are
illustrated in Figure 12, where rounded edges are used to make the curve
clear.

Figure 12: The curve fills one-eighth of the plane.

First let us determine exactly which lattice points are hit.

######  Theorem 31.

We have $(x,y)=(s(n),t(n))$ for $(x,y)\in\mathbb{N}\times\mathbb{N}$ if and
only if $x\geq y$ and $(x,y)\not=(0,0)$ and $x\equiv y\ \mbox{\rm(mod}\
2\mbox{\rm)}$. Furthermore, for each such pair $(x,y)$, there are at most two
such $n$.

###### Proof.

We use the following Walnut code:

    def even2 "Ek n=2*k":
    def curve "?msd_4 $rss(n,x) & $rst(n,y)":
    eval curvecheck "?msd_4 Ax,y (?msd_2 x>=y & x+y>0 & $even2(?msd_2 x-y)) <=>
       En $curve(n,x,y)":
    eval curvecheck3 "?msd_4 Ex,y,n1,n2,n3 n1<n2 & n2<n3 &
       $curve(n1,x,y) & $curve(n2,x,y) & $curve(n3,x,y)":

The first check returns TRUE and the second, asserting a point that is hit
three times, returns FALSE. ∎

######  Theorem 32.

The curve defined by $(P_{n})_{n\geq 0}$ is not self-intersecting.

###### Proof.

Because of the parity condition on $x,y$ in the pairs visited it suffices to
show that we never traverse the same segment $(P_{n},P_{n+1})$ twice for
different $n$, either in the same direction, or the reverse direction. We do
this as follows: we assert the existence of these traversals.

    eval selfint1 "?msd_4 Em,x1,y1,x2,y2,n $curve(m,x1,y1) &
       $curve(m+1,x2,y2) & $curve(n,x1,y1) & $curve(n+1,x2,y2) & m!=n":

    eval selfint2 "?msd_4 Em,x1,y1,x2,y2,n $curve(m,x1,y1) &
       $curve(m+1,x2,y2) & $curve(n+1,x1,y1) & $curve(n,x2,y2) & m!=n":

And Walnut returns FALSE for both. ∎

##  11 Going further

Since, as mentioned in the introduction, $a(n)$ is $+1$ or $-1$, according to
whether the number of $11$’s occurring in $(n)_{2}$ are even or odd, this
suggests considering the analogous function $a^{\prime}(n)$, where we instead
count the number of $00$’s occurring in $(n)_{2}$. Then it is easy to see that
$a^{\prime}(n)$ obeys the recursion

$\displaystyle a^{\prime}(2n)$ $\displaystyle=(-1)^{n+1}a^{\prime}(n)$
$\displaystyle\quad(n\geq 1);$ $\displaystyle a^{\prime}(2n+1)$
$\displaystyle=a^{\prime}(n)$ $\displaystyle\quad(n\geq 0),$

with initial condition $a^{\prime}(0)=1$. Then, in analogy with $s(n)$ and
$t(n)$, one can consider the sums

$\displaystyle s^{\prime}(n)$ $\displaystyle=\sum_{0\leq i\leq
n}a^{\prime}(n)$ $\displaystyle t^{\prime}(n)$ $\displaystyle=\sum_{0\leq
i\leq n}(-1)^{n}a^{\prime}(n).$

The first few values of these sequences are given in Table 2.

$n$ | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
$a^{\prime}(n)$ | 1 | 1 | 1 | 1 | $-1$ | 1 | 1 | 1 | 1 | $-1$ | 1 | 1 | $-1$ | 1 | 1 | 1
$s^{\prime}(n)$ | 1 | 2 | 3 | 4 | 3 | 4 | 5 | 6 | 7 | 6 | 7 | 8 | 7 | 8 | 9 | 10
$t^{\prime}(n)$ | 1 | 0 | 1 | 0 | $-1$ | $-2$ | $-1$ | $-2$ | $-1$ | 0 | 1 | 0 | $-1$ | $-2$ | $-1$ | $-2$
Table 2: First few values of $a^{\prime}(n)$, $s^{\prime}(n)$, and
$t^{\prime}(n)$.

It turns out that both $s^{\prime}(n)$ and $t^{\prime}(n)$ are synchronized
functions, which makes it possible to carry out the same kinds of analysis
that we did for the Rudin-Shapiro sequence. However, since $t^{\prime}(n)$
takes negative values, it’s easier to work with $1-t^{\prime}(n)$ instead.
Then it is possible to prove that both $s^{\prime}(n)$ and $1-t^{\prime}(n)$
are $(4,2)$-synchronized.

We just mention a few results without proof, leaving proofs and further
explorations to the reader.

######  Theorem 33.

  * (a)

We have

$\displaystyle s^{\prime}(2n)$
$\displaystyle=s^{\prime}(n-1)-t^{\prime}(n)+2,$ $\displaystyle\quad(n\geq 1)$
$\displaystyle s^{\prime}(2n+1)$
$\displaystyle=s^{\prime}(n)-t^{\prime}(n)+2,$ $\displaystyle\quad(n\geq 0)$
$\displaystyle t^{\prime}(2n)$
$\displaystyle=-t^{\prime}(n)-s^{\prime}(n-1)+2,$ $\displaystyle\quad(n\geq
0)$ $\displaystyle t^{\prime}(2n+1)$
$\displaystyle=-t^{\prime}(n)-s^{\prime}(n)+2$ $\displaystyle\quad(n\geq 0).$

  * (b)

We have

$\displaystyle s^{\prime}(4n)$
$\displaystyle=2s^{\prime}(n)-(2-(-1)^{n})r^{\prime}_{n}+2,$
$\displaystyle\quad(n\geq 1)$ $\displaystyle s^{\prime}(4n+1)$
$\displaystyle=2s^{\prime}(n)-2r^{\prime}_{n}+2,$ $\displaystyle\quad(n\geq
0)$ $\displaystyle s^{\prime}(4n+2)$
$\displaystyle=2s^{\prime}(n)-r^{\prime}_{n}+2,$ $\displaystyle\quad(n\geq 0)$
$\displaystyle s^{\prime}(4n+3)$ $\displaystyle=2s^{\prime}(n)+2,$
$\displaystyle\quad(n\geq 0).$

  * (c)

For $k\geq 1$, the minimum value of $s^{\prime}(n)$ for $n\in[4^{k},4^{k+1})$
is $2^{k+1}-1$ and $s^{\prime}(n)$ attains this value only when
$n=(4^{k+1}-4)/3$.

For $k\geq 0$, the maximum value of $s^{\prime}(n)$ for $n\in[4^{k},4^{k+1})$
is $3\cdot 4^{k-1}-2$ and $s^{\prime}(n)$ attains this value only when
$n=4^{k+1}-1$.

  * (d)

For $n\geq 1$ we have $3\sqrt{n}/2\leq s^{\prime}(n)\leq\sqrt{75n/7}$.

  * (e)

$\liminf s^{\prime}(n)/\sqrt{n}=\sqrt{3}$.

  * (f)

For $n\geq 0$ we have $-\sqrt{24n/7}\leq t^{\prime}(n)\leq 0$.

Similarly, many of the results in [15] can be rederived using a
$(4,2)$-synchronized automaton for their summation function $S(N)$.

## Acknowledgments

We are grateful to Jean-Paul Allouche for several helpful suggestions.

## References

  * [1] J.-P. Allouche.  Automates finis en théorie des nombres.  Exposition. Math. 5 (1987), 239–266.
  * [2] J. Berstel and C. Reutenauer.  Noncommutative Rational Series With Applications, Vol. 137 of Encyclopedia of Mathematics and Its Applications.  Cambridge University Press, 2011.
  * [3] J. Brillhart and P. Morton.  Über Summen von Rudin-Shapiroschen Koeffizienten.  Illinois J. Math. 22 (1978), 126–148.
  * [4] J. Brillhart and P. Erdős and P. Morton.  On sums of Rudin-Shapiro coefficients. II.  Pacific J. Math. 107 (1983), 39–69.
  * [5] J. Brillhart and P. Morton.  A case study in mathematical research: the Golay-Rudin-Shapiro sequence.  Amer. Math. Monthly 103 (1996), 854–869.
  * [6] A. Carpi and C. Maggi.  On synchronized sequences and their separators.  RAIRO Inform. Théor. App. 35 (2001), 513–524.
  * [7] A. Cobham.  On the base-dependence of sets of numbers recognizable by finite automata.  Math. Systems Theory 3 (1969), 186–192.
  * [8] A. Cobham.  Uniform tag sequences.  Math. Systems Theory 6 (1972), 164–192.
  * [9] F. M. Dekking, M. Mendès France, and A. J. van der Poorten.  Folds!  Math. Intelligencer 4 (1982), 130–138, 173–181, 190–195.  Erratum, 5 (1983), 5.
  * [10] M. J. E. Golay.  Multi-slit spectrometry.  J. Optical Soc. Amer. 39 (1949), 437–444.
  * [11] M. J. E. Golay.  Static multislit spectrometry and its application to the panoramic display of infrared spectra.  J. Optical Soc. Amer. 41 (1951), 468–472.
  * [12] J. E. Hopcroft and J. D. Ullman.  Introduction to Automata Theory, Languages, and Computation.  Addison-Wesley, 1979.
  * [13] J.-P. Kahane.  Some Random Series of Functions.  Cambridge Studies in Advanced Mathematics, Vol. 5, 2nd edition.  Cambridge University Press, 1994.
  * [14] J. Konieczny.  Gowers norms for the Thue-Morse and Rudin-Shapiro sequences.  Annales de l’Institut Fourier 69 (2019), 1897–1913.
  * [15] P. Lafrance, N. Rampersad, and R. Yee.  Some properties of a Rudin-Shapiro-like sequence.  Adv. Appl. Math. 63 (2015), 19–40.
  * [16] C. Mauduit and J. Rivat.  Prime numbers along Rudin-Shapiro sequences.  J. Eur. Math. Soc. 17 (2015), 2595–2642.
  * [17] M. Mendès France and G. Tenenbaum.  Dimension des courbes planes, papiers pliés et suites de Rudin-Shapiro.  Bull. Soc. Math. France 109 (1981), 207–215.
  * [18] M. Mendès France.  Paper folding, space-filling curves and Rudin-Shapiro sequences.  In Papers in Algebra, Analysis and Statistics, Vol. 9 of Contemporary Mathematics, Amer. Math. Society, 1982, pp. 85–95.
  * [19] H. Mousavi.  Automatic theorem proving in Walnut.  Arxiv preprint arXiv:1603.06017 [cs.FL], available at http://arxiv.org/abs/1603.06017, 2016.
  * [20] W. Rudin.  Some theorems on Fourier coefficients.  Proc. Amer. Math. Soc. 10 (1959), 855–859.
  * [21] J. Shallit.  Synchronized sequences.  In T. Lecroq and S. Puzynina, editors, WORDS 2021, Vol. 12847 of Lecture Notes in Computer Science, pp. 1–19. Springer-Verlag, 2021\.
  * [22] J. Shallit.  The Logical Approach To Automatic Sequences: Exploring Combinatorics on Words with Walnut, Vol. 482 of London Math. Society Lecture Note Series.  Cambridge University Press, 2022.
  * [23] J. Shallit.  Rarefied Thue-Morse sums via automata theory and logic.  Arxiv preprint ArXiv:2302.09436 [math.NT], February 18 2023, available at https://arxiv.org/abs/2302.09436.
  * [24] H. S. Shapiro.  Extremal problems for polynomials and power series.  Master’s thesis, MIT, 1951.
  * [25] N. J. A. Sloane et al.  The on-line encyclopedia of integer sequences, 2023.  Available at https://oeis.org.