LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-14

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Base-b digit cylinders are orbit cylinders

Statement

Assume the Axiom of Countable Choice. Fix $b \geq 2$ and a word $w = (w_{1}, \dots, w_{ℓ})$ , and put

$m = \sum_{r = 1}^{ℓ} w_{r} b^{ℓ - r} .$

Away from

$E_{b} = {k / b^{q} : q \geq 0, 0 \leq k < b^{q}} \subseteq [0, 1),$

for every $x \in [0, 1) ∖ E_{b}$ and $j \geq 1$ , the word $w$ begins at digit $j$ of $x$ if and only if

$D_{b}^{j - 1} x \in [m / b^{ℓ}, (m + 1) / b^{ℓ}) .$

The canonical convention selects a single expansion at every point of $E_{b}$ , and $E_{b}$ is countable and Lebesgue null.

Facts & Assumptions

Given: Countable choice, an integer $b \geq 2$ , a length $ℓ \geq 1$ , the word $w$ , and $j \geq 1$ .

[F1]

The canonical digits satisfy $D_{b}^{r} x = b D_{b}^{r - 1} x - d_{r}^{(b)} (x)$ and use the terminating expansion at $b$ -adic points (Canonical base-b expansions and normal numbers).

[F2]

The level- $ℓ$ intervals $[h / b^{ℓ}, (h + 1) / b^{ℓ})$ partition $[0, 1)$ , and $D_{b}^{ℓ}$ is affine on each such interval (Integer-base maps and b-adic circle intervals).

[F3]

A countable union of countable sets is countable under countable choice (Countable unions of at most countable sets, assuming ${A C}_{ω}$ ), and a countable subset of $R$ is Lebesgue null (Every at most countable subset of $R^{n}$ is Lebesgue null; in particular $λ_{1} (Q) = 0$ ).

Proof

technique · direct digit calculation

1.1

Put $y = D_{b}^{j - 1} x$ . Iterating the recurrence in [F1] for $ℓ$ places gives $y = \sum_{r = 1}^{ℓ} d_{j + r - 1}^{(b)} (x) b^{- r} + b^{- ℓ} D_{b}^{j + ℓ - 1} x .$

2.1

Since the last iterate lies in $[0, 1)$ , the first sum equals $h / b^{ℓ}$ , where $h = \sum_{r = 1}^{ℓ} d_{j + r - 1}^{(b)} (x) b^{ℓ - r}$ , and $h / b^{ℓ} \leq y < (h + 1) / b^{ℓ} .$

step 1.1algebra

3.1

By the disjoint half-open partition in [F2], $y$ belongs to the interval $[m / b^{ℓ}, (m + 1) / b^{ℓ})$ exactly when $h = m$ . Uniqueness of positional representation for the integers $0 \leq h, m < b^{ℓ}$ says this is equivalent to $(d_{j}^{(b)} (x), \dots, d_{j + ℓ - 1}^{(b)} (x)) = w$ . This in fact holds also at the endpoints under the canonical half-open convention, and therefore implies the claimed equivalence away from $E_{b}$ .

F1F2step 2.1

4.1

For each $q$ , the set ${k / b^{q} : 0 \leq k < b^{q}}$ is finite. Hence $E_{b}$ is a countable union of finite sets, so [F3] makes it countable and Lebesgue null. At each of its points [F1] chooses the terminating string and excludes the eventually- $(b - 1)$ string. Countable choice is used precisely through the two published countability/nullity suppliers in [F3], not in the digit calculation.

F1F3step 3.1∎

Depends on

Used by

Borel's exceptional set can be uncountable and null Example
Birkhoff averages need not converge at every point False statement
Borel's normal number theorem Theorem

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Charles Walkden, Ergodic Theory lecture notes (standard reference, not scraped)