Isaac's Condition (TU) is false

Ralf Stephan

math.NT Oct 15, 2026 · v1

Read PDF arXiv abstract Code

TL;DR

All definitions, lemmas and both proofs refuting Isaac's Condition (TU) are formalized in Lean 4 with Mathlib; two cited theorems enter as axioms.

Abstract

In 2006 Isaac reduced the simple normality to base $2$ of $\sqrt s$, for $s$ not a perfect square, to a property of dyadic expansions that he called Condition (TU): the upper frequency of the digit $1$ in $\sqrtν$, along any subsequence, depends only on the tail of the expansion of $ν$. We show that Condition (TU) is false, already for the full sequence. We give two proofs. The first is elementary and turns Isaac's own reduction against the condition. The second uses the theorem of Kaufman and Mosquera–Shmerkin on the Fourier decay of smooth images of self-similar measures, and gives counterexamples for almost every point of a Cantor measure. All results are machine-verified in Lean 4; the second proof uses the two cited theorems as hypotheses.

Problem

In 2006 Isaac reduced the simple normality to base 2 of square roots of non-squares to a property he called Condition (TU). It states that the upper frequency of the digit 1 in the dyadic expansion of sqrt(ν) depends only on the tail of ν's expansion. Whether Condition (TU) holds determines whether Isaac's claimed proof is valid.

Approach

The first proof is elementary. It turns Isaac's own reduction into a bootstrap that builds a sparse dyadic series x for which the pair (x^2, x^2+1/4) would violate (TU). The second proof uses the Mosquera–Shmerkin Fourier-decay theorem and the Davenport–Erdős–LeVeque criterion on a ratio-1/8 Cantor measure. This yields explicit counterexamples for almost every point of the measure. Everything is formalized in Lean 4 with Mathlib in the file BB47/Isaac.lean, with the two cited theorems stated as axioms.

Results

Condition (TU) is false, already for the full sequence n_i = i, so the simple normality of sqrt(2) to base 2 remains open. The first proof is verified using only Lean's standard axioms. The second proof additionally relies on exactly the two cited theorems.

Statement	Lean declaration
Definition 2.1	TU, TUfull, SameTail, freq
Proposition 3.1	frequently_freq_ge
Theorem 1.1, first proof	not_TUfull_bootstrap, not_TU_bootstrap
Theorem 4.1 (axiom)	MS.fourierDecay_smoothImage
Theorem 1.1, second proof	not_TUfull_fourier

Correspondence between paper statements and Lean declarations (excerpt)

Papers With

Isaac's Condition (TU) is false