Critical exponent of infinite balanced words via the Pell number system (Q2333033)

The \textit{critical exponent} of an infinite word \(w\) is the supremum of the set of all rational numbers \(r\) such that there exists a finite nonempty factor of \(w\) with exponent \(r\). \textit{N. Rampersad} et al. [Theor. Comput. Sci. 777, 454--463 (2019; Zbl 1446.68132)] conjectured that the smallest possible critical exponent of an infinite balanced word over a \(5\)-letter alphabet is \(3/2\) (note that a general conjecture was given for a \(k\)-letter alphabet). In the paper under review, this conjecture for a \(5\)-letter alphabet is proved using ``automatic theorem proving'' techniques. The authors make use of the Walnut package based on Büchi's theorem and first-order logic. A numeration system based on Pell numbers \(1,2,5,12,29,70,\dots\) is related to the studied infinite word. To be able to use the formalism of first-order logic and encode this infinite word in an extension of Presburger arithmetic, the authors obtain an automaton that recognizes the addition relation for words in that numeration system. This is again a nice example of how computational techniques are used in combinatorics on words. For the entire collection see [Zbl 1419.68014].