Orbit gaps for powers of quadratic Pisot numbers

For a quadratic Pisot number α>1, how can the fractional parts of ξαⁿ fail to be uniformly distributed? The studied criterion concerns roots of X²−aX−b and coefficients ξ in the paper’s class C(α).

Why it matters and what counts as progress

Why it matters: A sufficient gap criterion gives concrete partial information on a wider non-equidistribution problem that remains open.

What counts as progress: An explicit interval missed by each allowed orbit under A(α)<1, or a stronger criterion, retaining the restriction on ξ and the quadratic conjugate.

How the problem developed

1993 · Open problem [1][2]
Michel Mendès France Restated the classical question of whether powers of rational numbers greater than one are dense modulo one; Bugeaud later formulated the broader Pisot-number version as Problem 10.61.
31 Aug 2026 · Criterion [3][4]
Ralf Stephan; Claude Opus 5 agents Registered a Lean-formalized criterion for quadratic Pisot numbers: under a stated exponent condition, every orbit in the associated Cantor set misses an open interval; the paper gives α=2+√5 as an instance.

AI contribution

AI-led Lean proof gives a quadratic orbit-gap criterion

For a quadratic real root α>1 of X²−aX−b whose conjugate has modulus below one, the Route A exponent condition A(α)<1 gives an open interval missed by every orbit (ξαⁿ mod 1) with ξ in the paper’s class C(α), so none is uniformly distributed. The criterion is equivalent to (log₂α−1)(log₂(α/|b|)−1)>1 and yields an explicit gap for α=2+√5.

AI involvementAI-led

ImportanceModest

Technical verificationFormal (Lean 4/Mathlib kernel and Comparator)

Human understandingFew