The exponent $1/4$ in three complexity bounds: integer bases, continued fractions, and the $(3/2)^n$ steering word

Source abstract

Let $ξ$ be a real algebraic irrational number and $p(n,ξ,b)$ the number of distinct blocks of length $n$ in its base-$b$ expansion. Bugeaud and Evertse proved in 2008 that $p(n,ξ,b)/(n(\log n)^η)$ is unbounded for every $η 0$. Finally, the subword complexity of the steering word of $(3/2)^n$ exceeds $C\,k(\log k)^η$ infinitely often for every $η<1/4$ and every $C$. The three proofs share one count: $\varepsilon^{-1}$ classes times $\varepsilon^{-3}$ subspaces from the quantitative Subspace Theorem of Evertse and Ferretti. The subspaces are then disposed of at the cost of a logarithm, with no further power of $\varepsilon^{-1}$. All three results, and the quantitative Subspace Theorem they rest on, are machine-verified in Lean~4.