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

Technical Summary: Superlinear Complexity of the $(3/2)^n$ Steering Word

Problem Statement
The paper investigates the symbolic dynamics generated by the orbit of the number 1 under the map $x \mapsto \frac{3}{2}x$, specifically focusing on the sequence of nearest-integer rounding errors. While the distribution of the sequence $\|(\frac{3}{2})^n\|$ (distance to the nearest integer) is a long-standing open problem in number theory, this work shifts focus to the "steering word" $T = (t_n)_{n \geq 0}$. This word records the integer translates selected at each step of the autonomous dynamics, defined by $t_n = 2m_{n+1} - 3m_n$, where $m_n = \text{round}((\frac{3}{2})^n)$. The central question addressed is the subword complexity $p_T(k)$, which counts the number of distinct factors of length $k$ in $T$. The paper aims to prove that this complexity is superlinear, meaning $\lim_{k \to \infty} p_T(k)/k = \infty$.

Methodology
The proof strategy is structured into three distinct stages, transferring methods from the study of algebraic number complexity (specifically the Adamczewski–Bugeaud method) to this dynamical setting. The argument relies heavily on the Subspace Theorem and is noted to be fully formalized in Lean-4.

1. Stage 0: Exact Identities and Unconditional Bounds (Sections 2)
   The author derives an exact "repetition identity." If a factor of length $k$ repeats at positions $a$ and $c$ ($a < c$), it forces the relation $3^k(\varepsilon_c - \varepsilon_a) = 2^k(\varepsilon_{c+k} - \varepsilon_{a+k})$, where $\varepsilon_n$ is the rounding error.

   • This identity yields a divisibility condition: $2^k \mid (m_c - m_a)$.
   • Combined with the growth properties of the orbit, this establishes that long repetitions cannot occur arbitrarily late in the word.
   • Unconditional Result: The paper proves $T$ is not eventually periodic and establishes a linear lower bound $p_T(k) \geq \frac{41}{24}k - 3$, which is strictly above the Morse–Hedlund floor ($k+1$) for aperiodic words.

2. Stage 1: Reduction to a Diophantine Kernel (Section 3)
   The problem of proving superlinear complexity is reduced to a single Diophantine statement, referred to as the Kernel (K).

   • Statement (K): For every rational $\theta \in (0, 1)$, the set of pairs $(a, c)$ with $2 \leq a < c$ satisfying $\|(\frac{3}{2})^c - (\frac{3}{2})^a\| \leq \theta^c$ is finite.
   • This represents an "exponential pair repulsion" property, improving the trivial lower bound of the distance between orbit points from base $2^{-1}$ to an arbitrary base $\theta < 1$.
   • The reduction shows that if (K) holds, then $p_T(k)/k \to \infty$.

3. Stage 2: Establishing the Kernel (Sections 4 & 5)
   The proof of (K) is achieved by partitioning the set of potential solutions into three "slices" and applying deep results from Diophantine approximation:

   • Bounded Gap Slice: For fixed gaps $c-a$, finiteness is proven using the Corvaja–Zannier Main Theorem (a consequence of the Schmidt Subspace Theorem).
   • Huge-Gap Slice: For the region where $a \leq \epsilon' c$, finiteness is also established via the Corvaja–Zannier theorem by treating the problem as a specific case of pseudo-Pisot exclusion.
   • Middle Band: For the remaining region where gaps grow but $a$ is not negligible compared to $c$, the author employs a gap dichotomy. If the set of solutions were infinite, one could extract a subfamily with distinct gaps. This leads to a contradiction via the Nair–Kumar–Rout S-unit tuple theorem, which would imply that $(\frac{3}{2})^c$ is an integer for some $c$, an impossibility.

Key Contributions and Results

• Main Theorem (Theorem 1.1): The subword complexity of the steering word $T$ is superlinear ($p_T(k)/k \to \infty$).
• Unconditional Lower Bound: The paper provides an explicit, unconditional linear lower bound $p_T(k) \geq \frac{41}{24}k - 3$, derived without relying on unproven conjectures.
• Formalization: The entire argument is formalized in Lean-4. The formalization depends only on the Evertse–Schlickewei Subspace Theorem in 3 variables, thereby confirming the correctness of the dependencies on the Corvaja–Zannier and Nair–Kumar–Rout results.
• Aperiodicity: A rigorous proof that the steering word is not eventually periodic.

Significance and Claims
The paper claims to resolve the complexity question for this specific autonomous dynamical system by bridging symbolic dynamics and Diophantine approximation.

• Methodological Transfer: It successfully adapts the Adamczewski–Bugeaud method, typically used for algebraic numbers, to a dynamical word. The author notes that the autonomous nature of the $(3/2)$-dynamics simplifies the bookkeeping, allowing repeated factors to compress into clean Diophantine inequalities without prefix-anchoring.
• Reliance on Deep Theorems: The proof of superlinearity is conditional on the Corvaja–Zannier theorem (refereed) and the Nair–Kumar–Rout theorem (a preprint at the time of writing). However, the Lean-4 formalization serves as a verification that these dependencies are logically sound consequences of the Subspace Theorem.
• Limitations: The results regarding the superlinear growth are ineffective; the Subspace Theorem does not provide explicit bounds on the size of the exceptional sets (the number of solutions to the Diophantine inequalities). The paper does not claim to solve the broader open problem regarding the density of $\|(\frac{3}{2})^n\| \to 0$, but rather characterizes the combinatorial complexity of the rounding sequence.