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.

Disclosure

“7. Acknowledgements The author thanks P. S. Nair, V. Kumar and S. S. Rout for their prompt response to the counterexample of Remark 5.4 and for the corrected state- ment recorded in Remark 5.5. The author utilized Claude Code as an AI coding assistant to aid in the Lean 4 formalization of the proofs presented in this paper. The author directed and reviewed all generated code and takes full responsibility for the mathematical integrity and final content of”

PDF page 19

Classification

Code generation, completion, or debugging

Multiplier

2

Verified

2026-08-23T18:51:41.537310Z

Structural counts