← All papers
First page of The Evertse-Ferretti interval result for a set of weights, and the exponent $1/2$ in three complexity bounds

The Evertse-Ferretti interval result for a set of weights, and the exponent $1/2$ in three complexity bounds

Ralf Stephan

math.NT Nov 12, 2026 · v1
All results, including an Evertse-Ferretti interval theorem for weight sets and three complexity bounds, are machine-verified in Lean 4 with Mathlib (GitHub repository).
The interval result of Evertse and Ferretti (2013) concerns a tuple $L$ of linear forms and one tuple $c$ of weights. It says that the parameters $Q$ for which the twisted height $H_{L,c,Q}$ has a small value outside an exceptional subspace $T(L,c)$ lie in $O(δ^{-2}\logδ^{-1})$ intervals $[Q_i,Q_i^ω)$. We prove this for a whole set $\mathcal{C}$ of weights with the same forms. At most $J$ subspaces $T(L,c)$ occur, where $J$ depends only on the dimension and on the number of places, and one family of $O(δ^{-2}\logδ^{-1})$ intervals serves every $c\in\mathcal{C}$ at once. Neither count depends on $\mathcal{C}$. In applications of Bugeaud-Evertse type the solutions are sorted into about $\varepsilon^{-1}$ classes with the same forms and different weights, and one application now serves all classes. We deduce three complexity bounds. For a real algebraic irrational number $ξ$, the number $p(n,ξ,b)$ of blocks of length $n$ in its base-$b$ expansion satisfies $\limsup p(n,ξ,b)/(n(\log n)^η)=\infty$ for every $η<1/2$; Bugeaud and Evertse proved this for $η<1/11$. The same holds for the continued fraction expansion of an algebraic number of degree at least three, and for the steering word of $(3/2)^n$. We explain why $1/2$ is the limit of the method. All results are machine-verified in Lean 4.

The Evertse-Ferretti interval result for twisted heights is stated for a single tuple of weights. In Bugeaud-Evertse style complexity bounds, solutions fall into about ε^{-1} classes with the same forms and different weights, and each class costs a separate application.

The interval result is extended to a whole set of weights sharing the same linear forms. The proof shows that at most J exceptional subspaces occur and that one family of O(δ^{-2} log δ^{-1}) intervals serves every weight in the set. Neither count depends on the set of weights. This is applied to complexity bounds for algebraic numbers, and every numbered statement is formalized in Lean 4 with Mathlib using only the standard axioms.

For algebraic irrational ξ, the base-b block complexity satisfies limsup p(n)/(n(log n)^η) = ∞ for every η < 1/2, improving Bugeaud-Evertse's 1/11. Analogous bounds hold for continued fractions of algebraic numbers of degree at least three and for the steering word of (3/2)^n. The paper argues that 1/2 is the limit of the method.