Aperiodicity and subword complexity in the binary expansion of powers of three

Ralf Stephan

math.CO Jul 16, 2026 · v3 math.NT

formalization number-theory combinatorics mathlib

Read PDF arXiv abstract Code

TL;DR

All theorems, including Stewart's classical bounds and the two new results on binary digits of 3^m, are verified in Lean 4/Mathlib, with Baker–Wüstholz taken as a cited axiom.

Abstract

We prove two results on the fine structure of the binary digits of $3^{m}$. First, for every fixed period $p$, the number of positions at which the binary expansion of $3^{m}$ breaks $p$-periodicity grows in order like $\log m/\log\log m$; equivalently, no window of the expansion deeper than a fixed power of $\log m$ is $p$-periodic. Second, the finite binary word formed by the low-order digits of $3^{m}$ has full low-order subword complexity: its complexity function satisfies $p_{3^{m}}(n)\ge n+1$ for every length $n$, once $m$ is large enough.

Problem

The work studies the fine structure of the binary digits of 3^m. It asks how often the expansion breaks p-periodicity, and whether the low-order digit word has full subword complexity.

Approach

A long periodic stretch in the binary expansion of 3^m yields a small nonzero linear form in logarithms. The Baker–Wüstholz theorem bounds such forms from below, with the explicit constant C(4,1). A geometric window-tiling scheme turns 'one break per window' into a growth rate. A finite Morse–Hedlund lemma, proved by determinism propagation, links low factor complexity to periodicity. Everything is formalized in Lean 4 with Mathlib, with Baker–Wüstholz as a cited axiom.

Results

The number of period-p breaks in 3^m is at least log m/(log log m + C_p) − 2, with effective constants. The subword complexity satisfies p_{3^m}(n) ≥ n+1 for all sufficiently large m. Both results are machine-checked in Lean.

Papers With

Aperiodicity and subword complexity in the binary expansion of powers of three