Superlinear complexity of the $(3/2{)}^n$ steering word

Abstract

Write $(3/2{)}^n=m_n+{\epsilon }_n$ with $m_n$ the nearest integer and ${\epsilon }_n\in [-\frac{1}{2},\frac{1}{2})$, and let $T=(t_n)$, $t_n=2m_{n+1}-3m_n$, be the resulting \emph{steering word}: the step-by-step record of the map $x\mapsto \frac{3}{2}x$ on the orbit of 1, coded by nearest-integer rounding. Using results by Corvaja--Zannier and Nair--Kumar--Rout we prove that the subword complexity $p_T(k)$ of $T$ is superlinear, $p_T(k)/k\to \infty$. The argument is completely formalized in Lean~4 and rests on a single external input, the Evertse--Schlickewei $S$-arithmetic subspace theorem, from which both cited results are themselves derived within the formalization.

added figures