math.NT — Number Theory

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

Contributed by Ralf Stephan

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. We prove that the subword complexity $p_T(k)$ of $T$ is superlinear, $p_T(k)/k\to\infty$. A pigeonhole argument reduces this to exponential pair repulsion of the orbit modulo one, which we establish by two applications of the $p$-adic Subspace Theorem: once in three variables, which handles all gaps between the two orbit points at once, and once in two variables (Ridout's theorem) for the single degenerate family of constant gap. The argument is completely formalized in Lean~4, together with the Subspace Theorem it uses.