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

Ralf Stephan

math.NT Jul 13, 2026 · v2

Read PDF arXiv abstract Code

TL;DR

The proof that the (3/2)^n steering word has superlinear subword complexity is fully formalized in Lean 4, depending only on the Subspace Theorem.

Abstract

Write $(3/2)^n = m_n + \eps_n$ with $m_n$ the nearest integer and $\eps_n\in[-\tfrac12,\tfrac12)$, and let $T=(t_n)$, $t_n=2m_{n+1}-3m_n$, be the resulting 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 $\pT(k)$ of $T$ is superlinear, $\pT(k)/k\to\infty$. The argument is completely formalized in Lean-4, depending only on the Subspace Theorem.

Problem

The symbolic dynamics of the map x↦(3/2)x on the orbit of 1, coded by nearest-integer rounding, produces a 'steering word' T. The question is how many distinct length-k factors T contains, i.e. its subword complexity.

Approach

Iterating the step relation telescopes into a closed-form circuit sum, yielding a repetition identity: equal length-k factors at positions a<c force exact Diophantine relations and divisibilities on the rounding errors. These reduce superlinearity to a Diophantine kernel about finiteness of near-repetition pairs, which is closed via a gap dichotomy using the Corvaja–Zannier and Nair–Kumar–Rout theorems, themselves consequences of the Schmidt/Evertse–Schlickewei subspace theorem. The entire argument is formalized in Lean 4.

Results

The subword complexity p_T(k) is superlinear: p_T(k)/k→∞. Unconditional slices also give p_T(k) ≥ (41/24)k − 3 and that T is not eventually periodic.

Papers With

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