Intertwining of Complementary Thue-Morse Factors

TL;DR

This paper investigates how factors and their binary complements occur within the Thue-Morse sequence, revealing two main intertwined patterns using logical formalization and automated theorem proving.

Contribution

It introduces a novel logical approach to analyze the occurrence patterns of factors and their complements in the Thue-Morse word.

Findings

Occurrences of factors and their complements are intertwined in two main ways.

Logical formalization enables automated proof of occurrence properties.

Provides a new method for analyzing combinatorial properties of automatic sequences.

Abstract

We consider the positions of occurrences of a factor $x$ and its binary complement $\overline{x}$ in the Thue-Morse word ${\bf t} = {\tt 01101001} \cdots$, and show that these occurrences are "intertwined" in essentially two different ways. Our proof method consists of stating the needed properties as a first-order logic formula $\varphi$, and then using a theorem-prover to prove $\varphi$.