The exponent $1/4$ in three complexity bounds: integer bases, continued fractions, and the $(3/2)^n$ steering word
Ralf Stephan
math.NT
Oct 22, 2026 · v1
TL;DR
All three complexity bounds and the quantitative Subspace Theorem are formalized in Lean 4 with Mathlib, released in a public repository with a declaration-by-declaration appendix.
Abstract
Let $ξ$ be a real algebraic irrational number and $p(n,ξ,b)$ the number of distinct blocks of length $n$ in its base-$b$ expansion. Bugeaud and Evertse proved in 2008 that $p(n,ξ,b)/(n(\log n)^η)$ is unbounded for every $η<1/11$. We prove this for every $η<1/4$. We also prove the analogous bound for the continued fraction expansion of an algebraic number of degree at least three, with every exponent $δ<1/4$. Bugeaud announced this statement in 2013 with an unspecified $δ>0$. Finally, the subword complexity of the steering word of $(3/2)^n$ exceeds $C\,k(\log k)^η$ infinitely often for every $η<1/4$ and every $C$. The three proofs share one count: $\varepsilon^{-1}$ classes times $\varepsilon^{-3}$ subspaces from the quantitative Subspace Theorem of Evertse and Ferretti. The subspaces are then disposed of at the cost of a logarithm, with no further power of $\varepsilon^{-1}$. All three results, and the quantitative Subspace Theorem they rest on, are machine-verified in Lean 4.
Problem
Bugeaud and Evertse showed that the block complexity p(n,ξ,b) of a real algebraic irrational ξ satisfies limsup p/(n(log n)^η)=∞ only for η<1/11. The paper seeks to raise this exponent and to prove analogous bounds for continued fraction expansions of algebraic numbers of degree at least three, and for the steering word of (3/2)^n.
Approach
The three proofs share one count: ε^{-1} classes of points times ε^{-3} subspaces, taken from the quantitative Subspace Theorem of Evertse and Ferretti. The subspaces are then handled at the cost of only a logarithm, using window arguments and Ridout's theorem on planes of constant gap. All results, including the quantitative Subspace Theorem, are formalized in Lean 4 on Mathlib using only the standard axioms.
Results
The exponent improves to every η<1/4 for integer bases, and the paper proves the continued-fraction bound for every δ<1/4 and the steering-word bound for every η<1/4. An intermediate 1/7 result is also machine-verified, and the formalization is public at github.com/rwst/Subspace-Theorems.
