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

Abstract

Write $(3/2)^n = m_n + \varepsilon_n$ with $m_n$ the nearest integer and $\varepsilon_n\in[-\tfrac12,\tfrac12)$, 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\tfrac32 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.