Automatic Sequences in Negative Bases and Proofs of Some Conjectures of Shevelev

TL;DR

This paper explores negative base automatic sequences using an extended theorem-prover, enabling proofs of conjectures about bi-infinite sequences and resolving open problems in the field.

Contribution

It introduces a method to handle negative bases in automatic sequences with Walnut, leading to proofs of conjectures and open problems in bi-infinite sequence theory.

Findings

Proved a strengthened version of Shevelev's theorem.

Resolved two open problems of Shevelev from 2017.

Reproved a 2000 result of Shur on bi-infinite binary words.

Abstract

We discuss the use of negative bases in automatic sequences. Recently the theorem-prover Walnut has been extended to allow the use of base (-k) to express variables, thus permitting quantification over Z instead of N. This enables us to prove results about two-sided (bi-infinite) automatic sequences. We first explain the theory behind negative bases in Walnut. Next, we use this new version of Walnut to give a very simple proof of a strengthened version of a theorem of Shevelev. We use our ideas to resolve two open problems of Shevelev from 2017. We also reprove a 2000 result of Shur involving bi-infinite binary words.