Prefixes of the Fibonacci word

Mignosi, Restivo, and Salemi (1998) proved that for all ϵ > 0 there exists an integer N such that all prefixes of the Fibonacci word of length ≥ N contain a suffix of exponent α 2 − ϵ , where α = ( 1 + 5 ) / 2 is the golden ratio. In this note we show how to prove an explicit version of this theorem using tools from automata theory and logic. Along the way we gain a better understanding of the repetitive structure of the Fibonacci word.