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.1F1

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.1step 1.1algebra

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^{ℓ} .$

3.1F1F2step 2.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}$ .

4.1F1F3step 3.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.

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

24 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)