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

Ralf Stephan

math.NT Jul 13, 2026 · v3

formalization number-theory combinatorics

Read PDF arXiv abstract Code

TL;DR

The full superlinear-complexity proof is formalized in Lean 4, assuming only the Evertse–Schlickewei subspace theorem as an axiom, with a public repository.

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 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.

Problem

The steering word T records nearest-integer rounding along the orbit of 1 under x ↦ (3/2)x. The goal is to determine whether its subword complexity p_T(k) grows faster than linearly.

Approach

An exact repetition identity shows that any repeated factor forces divisibility constraints and a Diophantine inequality on ‖(3/2)^c − (3/2)^a‖. Superlinearity is reduced to finiteness of a Diophantine kernel. The kernel is closed through a gap dichotomy, using the Corvaja–Zannier theorem and a corrected form of a Nair–Kumar–Rout S-unit result. All steps, including derivations of both cited results, are formalized in Lean 4 from the Evertse–Schlickewei subspace theorem as the single external input, with Claude Code used as a coding assistant.

Results

p_T(k)/k → ∞. Unconditional intermediate results show that T is not eventually periodic and that p_T(k) ≥ (41/24)k − 3. Each numbered statement corresponds to a Lean declaration in the accompanying repository.

Papers With

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