The number of primitive words of unbounded exponent in the language of an HD0L-system is finite

TL;DR

This paper proves that for any HD0L-system, only finitely many primitive words can be repeatedly extended to arbitrary powers within its language, with a formal proof in Isabelle/HOL.

Contribution

It establishes the finiteness of primitive words with unbounded exponents in HD0L-systems and formalizes the proof in Isabelle/HOL.

Findings

Finiteness of primitive words with unbounded powers in HD0L-systems

Application to factors of morphic words

Formal proof in Isabelle/HOL

Abstract

Let $H$ be an HD0L-system. We show that there are only finitely many primitive words $v$ with the property that $v^k$, for all integers $k$, is an element of the factorial language of $H$. In particular, this result applies to the set of all factors of a morphic word. We provide a formalized proof in the proof assistant Isabelle/HOL as part of the Combinatorics on Words Formalized project.