TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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.

The Cantor set is exactly the set of $\sum_{k \geq 1} a_{k} 3^{- k}$ with every $a_{k} \in {0, 2}$ , and this gives a bijection with ${0, 1}^{N}$

Statement

Let $D$ be the set of sequences $a : N \to {0, 2}$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences), the two values being the real numbers $0$ and $2$ . For $a \in D$ the series $\sum_{k \geq 0} a_{k} 3^{- k - 1}$ converges (Series, partial sums, convergence and the sum, divergence, and the tail series); write

$Φ (a) : = \sum_{k = 0}^{\infty} a_{k} 3^{- k - 1} .$

Then, with $C$ and $(C_{n})$ as in The Cantor middle-thirds set as the intersection of the sets $C_{n}$ obtained by removing open middle thirds:

$Φ (a) \in [0, 1]$ for every $a \in D$ , and $C = {Φ (a) : a \in D}$ ;
$Φ$ is injective, so $Φ$ is a bijection from $D$ onto $C$ (Injection, surjection, bijection);
consequently $b \mapsto Φ ((2 b_{k})_{k})$ is a bijection from ${0, 1}^{N}$ , the set of sequences with values in ${0, 1}$ , onto $C$ ;
$C = \frac{1}{3} C \cup (\frac{2}{3} + \frac{1}{3} C)$ , and the two sets on the right are disjoint.

On the indexing. The digit $a_{k}$ carries the weight $3^{- k - 1}$ , so the series starts at $k = 0$ with the term $a_{0} / 3$ ; written with the classical $1$ -based index it reads $\sum_{k \geq 1} a_{k} 3^{- k}$ , which is the form in the title. Sequences in this library are functions on $N$ and $N$ contains $0$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences), so the $0$ -based form is the one used throughout the proof.

Facts & Assumptions

Given: The sets $C_{n}$ and $C$ of The Cantor middle-thirds set as the intersection of the sets $C_{n}$ obtained by removing open middle thirds, the set $D$ of sequences with values in ${0, 2}$ , and for $a \in D$ the shifted sequence $σ a$ defined by $(σ a)_{k} : = a_{k + 1}$ , which again lies in $D$ .

[L1]

The Cantor set: $C_{0} = [0, 1]$ , $C_{n + 1} = \frac{1}{3} C_{n} \cup (\frac{2}{3} + \frac{1}{3} C_{n})$ , $C = ⋂_{n} C_{n} = ⋂_{n} C_{n + 1}$ , every $C_{n} \subseteq [0, 1]$ , the two halves of $C_{n + 1}$ lie in $[0, \frac{1}{3}]$ and in $[\frac{2}{3}, 1]$ respectively and are disjoint, and $3^{- n}$ denotes $(3^{- 1})^{n}$ (The Cantor middle-thirds set as the intersection of the sets $C_{n}$ obtained by removing open middle thirds, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L2]

Series: partial sums $s_{n} = \sum_{k < n} t_{k}$ , convergence of $(s_{n})$ , the sum as its limit, the tail clause $\sum_{k \geq m} t_{k}$ and the identity $\sum_{k < n + 1} t_{k} = t_{0} + \sum_{j < n} t_{j + 1}$ (Series, partial sums, convergence and the sum, divergence, and the tail series, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L3]

A series of nonnegative terms converges exactly when its partial sums are bounded above, its sum is then their supremum, every partial sum is at most the sum, and a convergent series of nonnegative terms has sum $\geq 0$ (A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum).

[L4]

$\sum_{k = 0}^{\infty} 3^{- k} = 1 / (1 - 3^{- 1}) = 3 \cdot 2^{- 1}$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges, Integer powers $a^{m}$ , Laws of integer exponents).

[L5]

Convergent series add and scale termwise (Convergent series add and scale termwise).

[L6]

Recursion and induction on $N$ (The recursion theorem, The principle of mathematical induction).

[L7]

Every nonempty subset of $N$ has a least element (The well-ordering principle).

[L8]

$3^{- n} \to 0$ (For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ ); convergence is tested against rational $ε > 0$ and a convergent sequence has exactly one limit (Limits and Cauchy sequences of reals, A sequence has at most one limit); $∣ z ∣ \geq 0$ and $∣ z ∣ = z$ for $z \geq 0$ (Basic properties of the absolute value).

[L9]

Ordered-field arithmetic: $0 < 1$ , so $2 > 0$ and $3 > 0$ and $3^{- 1} > 0$ , and $3^{- 1} < 2 \cdot 3^{- 1}$ ; adding a constant and multiplying by a positive preserve an inequality; the order is total and transitive (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Ordered field, Complete ordered field (least-upper-bound property)). These order-arithmetic facts are stated by their sources for the strict order only; the nonstrict forms used below follow by adjoining the equality case, in which the two sides coincide.

Proof

technique · direct

1.1

$Φ$ is well defined and takes values in $[0, 1]$ . For $a \in D$ every term $a_{k} 3^{- k - 1}$ is $\geq 0$ by [L1] and [L9], and for every $n$ the partial sum satisfies $\sum_{k < n} a_{k} 3^{- k - 1} \leq \sum_{k < n} 2 \cdot 3^{- 1} \cdot 3^{- k} = 2 \cdot 3^{- 1} \sum_{k < n} 3^{- k} \leq 2 \cdot 3^{- 1} \cdot 3 \cdot 2^{- 1} = 1$ , by [L3], [L4] and [L9]. So by [L3] the series converges, its sum $Φ (a)$ satisfies $0 \leq Φ (a) \leq 1$ , and $Φ (a) \in [0, 1]$ by [L1].

givenL1L3L4L9

1.2

Shift identity: $Φ (a) = a_{0} \cdot 3^{- 1} + 3^{- 1} Φ (σ a)$ for every $a \in D$ . Indeed by [L2] the partial sums satisfy $\sum_{k < n + 1} a_{k} 3^{- k - 1} = a_{0} 3^{- 1} + \sum_{j < n} a_{j + 1} 3^{- j - 2} = a_{0} 3^{- 1} + 3^{- 1} \sum_{j < n} a_{j + 1} 3^{- j - 1}$ , using $3^{- j - 2} = 3^{- 1} \cdot 3^{- j - 1}$ from [L1] and [L9]; letting $n$ grow and using [L5] and [L2] gives the identity.

givenL1L2L5L9

1.3

Self-similarity of $C$ , claim 4. If $y \in C$ then $y \in C_{n}$ for every $n$ , so $y \cdot 3^{- 1} \in \frac{1}{3} C_{n} \subseteq C_{n + 1}$ and $2 \cdot 3^{- 1} + y \cdot 3^{- 1} \in \frac{2}{3} + \frac{1}{3} C_{n} \subseteq C_{n + 1}$ for every $n$ , whence both lie in $⋂_{n} C_{n + 1} = C$ by [L1]; this gives the inclusion $\supseteq$ . Conversely let $x \in C$ , so $x \in C_{n + 1}$ for every $n$ . By [L1] the first half of $C_{n + 1}$ lies in $[0, \frac{1}{3}]$ and the second in $[\frac{2}{3}, 1]$ , and $\frac{1}{3} < \frac{2}{3}$ by [L9]. If $x \leq \frac{1}{3}$ then $x \notin [\frac{2}{3}, 1]$ , so for every $n$ one has $x \in \frac{1}{3} C_{n}$ , that is $3 x \in C_{n}$ ; hence $3 x \in C$ and $x \in \frac{1}{3} C$ . If $x > \frac{1}{3}$ then $x \notin [0, \frac{1}{3}]$ , so for every $n$ one has $x \in \frac{2}{3} + \frac{1}{3} C_{n}$ , that is $3 x - 2 \in C_{n}$ ; hence $3 x - 2 \in C$ and $x \in \frac{2}{3} + \frac{1}{3} C$ . Disjointness is [L1] and [L9], since $\frac{1}{3} C \subseteq [0, \frac{1}{3}]$ and $\frac{2}{3} + \frac{1}{3} C \subseteq [\frac{2}{3}, 1]$ .

L1L9

2.1

$Φ (a) \in C$ for every $a \in D$ . By induction on $n$ ([L6]) the statement "for every $a \in D$ , $Φ (a) \in C_{n}$ " holds for every $n$ : at $n = 0$ it is step 1.1 and [L1]; and if it holds at $n$ , then for $a \in D$ the value $a_{0}$ is $0$ or $2$ , so step 1.2 gives $Φ (a) = 3^{- 1} Φ (σ a) \in \frac{1}{3} C_{n}$ in the first case and $Φ (a) = 2 \cdot 3^{- 1} + 3^{- 1} Φ (σ a) \in \frac{2}{3} + \frac{1}{3} C_{n}$ in the second, so $Φ (a) \in C_{n + 1}$ by [L1]. Hence $Φ (a) \in ⋂_{n} C_{n} = C$ .

step 1.1step 1.2L1L6

2.2

The digit recursion. Fix $x \in C$ and let $T : R \to R$ be $T (y) : = 3 y$ for $y \leq 3^{- 1}$ and $T (y) : = 3 y - 2$ for $y > 3^{- 1}$ , a definition by cases on the total order ([L9]) and so a genuine function. By [L6] there is $y : N \to R$ with $y_{0} = x$ and $y_{n + 1} = T (y_{n})$ ; put $a_{n} : = 0$ when $y_{n} \leq 3^{- 1}$ and $a_{n} : = 2$ otherwise, so that $a \in D$ and $y_{n + 1} = 3 y_{n} - a_{n}$ for every $n$ . Every $y_{n}$ lies in $C$ , by induction on $n$ : $y_{0} = x \in C$ ; and if $y_{n} \in C$ then, by step 1.3, either $y_{n} \in \frac{1}{3} C \subseteq [0, \frac{1}{3}]$ or $y_{n} \in \frac{2}{3} + \frac{1}{3} C \subseteq [\frac{2}{3}, 1]$ , and these two cases are exactly $y_{n} \leq \frac{1}{3}$ and $y_{n} > \frac{1}{3}$ by [L9]; in the first $y_{n} = z \cdot 3^{- 1}$ with $z \in C$ and $y_{n + 1} = 3 y_{n} = z \in C$ , in the second $y_{n} = 2 \cdot 3^{- 1} + z \cdot 3^{- 1}$ with $z \in C$ and $y_{n + 1} = 3 y_{n} - 2 = z \in C$ .

step 1.3L1L6L9

2.3

$Φ$ is injective. Let $a, b \in D$ with $a \neq b$ ; the set of $k$ with $a_{k} \neq b_{k}$ is a nonempty subset of $N$ , so by [L7] it has a least element $k$ , and by symmetry we may take $a_{k} = 0$ and $b_{k} = 2$ . By [L5], $Φ (b) - Φ (a) = \sum_{j \geq 0} (b_{j} - a_{j}) 3^{- j - 1}$ , and the terms with $j < k$ vanish, so by [L2] this equals $2 \cdot 3^{- k - 1} + R$ with $R : = \sum_{j \geq k + 1} (b_{j} - a_{j}) 3^{- j - 1}$ . Every $b_{j} - a_{j}$ is at least $- 2$ , so the series $\sum_{j \geq k + 1} ((b_{j} - a_{j}) + 2) 3^{- j - 1}$ has nonnegative terms and hence nonnegative sum by [L3], giving $R \geq - \sum_{j \geq k + 1} 2 \cdot 3^{- j - 1} = - 2 \cdot 3^{- k - 2} \cdot 3 \cdot 2^{- 1} = - 3^{- k - 1}$ by [L2], [L4], [L5] and [L9]. Therefore $Φ (b) - Φ (a) \geq 2 \cdot 3^{- k - 1} - 3^{- k - 1} = 3^{- k - 1} > 0$ and $Φ (a) \neq Φ (b)$ .

step 1.1L2L3L4L5L7L9

3.1

The value is recovered from the digits. With $x$ , $(y_{n})$ and $a$ as in step 2.2, put $s_{n} : = \sum_{k < n} a_{k} 3^{- k - 1}$ . Then $x = s_{n} + 3^{- n} y_{n}$ for every $n$ , by induction on $n$ ([L6]): at $n = 0$ both sides are $x$ , since $s_{0} = 0$ by [L2] and $3^{0} = 1$ ; and if $x = s_{n} + 3^{- n} y_{n}$ then $s_{n + 1} + 3^{- n - 1} y_{n + 1} = s_{n} + a_{n} 3^{- n - 1} + 3^{- n - 1} (3 y_{n} - a_{n}) = s_{n} + 3^{- n} y_{n} = x$ , using [L1], [L2] and [L9].

step 2.2L1L2L6L9

4.1

Hence $x = Φ (a)$ , so $C \subseteq Φ [D]$ . Every $y_{n}$ lies in $C \subseteq [0, 1]$ by step 2.2 and [L1], so $0 \leq x - s_{n} = 3^{- n} y_{n} \leq 3^{- n}$ by step 3.1 and [L9]. Given a rational $ε > 0$ , [L8] supplies $N$ with $3^{- n} < ε$ for all $n \geq N$ , and then $∣ s_{n} - x ∣ = x - s_{n} \leq 3^{- n} < ε$ by [L8]; so $s_{n} \to x$ . But $s_{n} \to Φ (a)$ by [L2], since $(s_{n})$ is the sequence of partial sums of the series defining $Φ (a)$ , and limits are unique by [L8]; therefore $x = Φ (a)$ with $a \in D$ .

step 2.2step 3.1L1L2L8L9

5.1

By steps 2.1 and 4.1 the image of $D$ under $Φ$ is exactly $C$ , which with step 1.1 is claim 1; step 2.3 is claim 2, so $Φ$ is a surjection from $D$ onto $C$ that is injective, that is, a bijection (Injection, surjection, bijection); the map $b \mapsto (2 b_{k})_{k}$ is a bijection from ${0, 1}^{N}$ onto $D$ , with inverse $a \mapsto (a_{k} \cdot 2^{- 1})_{k}$ by [L9], and a composition of bijections is a bijection, which is claim 3; and step 1.3 is claim 4.

step 1.1step 1.3step 2.1step 2.3step 4.1L9∎

Remarks

The endpoints are the digit sequences that are eventually constant. For instance $0 = Φ (0, 0, 0, \dots)$ , $1 = Φ (2, 2, 2, \dots)$ , $\frac{1}{3} = Φ (0, 2, 2, 2, \dots)$ and $\frac{2}{3} = Φ (2, 0, 0, 0, \dots)$ , the first two by For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges and the last two by the shift identity of step 1.2. That the eventually constant sequences do not exhaust $C$ is the content of $1 / 4$ lies in the Cantor set and is the endpoint of no removed interval, so the endpoints do not exhaust it ↗, where $1 / 4$ is computed to be $Φ (0, 2, 0, 2, \dots)$ .
No digit is ever $1$ , and that is the whole point. A real of $[0, 1]$ with a ternary expansion using the digit $1$ at some place and not representable without it lies in one of the removed middle thirds. The theorem does not assert that every real has a ternary expansion, and it does not need to: the map $Φ$ is constructed from the digits, and the converse direction extracts digits from a point of $C$ by the canonical recursion of step 2.2, never by invoking a general expansion theorem.
Where the choice-freeness lies. The digit extraction is a definition by cases on a total order fed to The recursion theorem, so the whole passage from a point of $C$ to its digit sequence is a single function, not a sequence of selections. The same discipline governs Every nonempty perfect subset of $R$ is uncountable and Baire category in $R$ , by nested intervals with canonically chosen rational endpoints: a countable intersection of dense open sets is dense, so $R$ is not a countable union of nowhere dense sets.
Claim 3 is what makes $C$ uncountable. ${0, 1}^{N}$ is in bijection with the power set of $N$ , which is uncountable by Cantor's theorem: $A ≺ P (A)$ ; that route and the perfect-set route are both recorded in The Cantor set is compact, perfect, uncountable, nowhere dense and of measure zero, and it contains no interval of positive length, so its only nonempty connected subsets are single points.

Depends on

Used by

Dependency tree · two levels

70 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

Cantor set (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 2 (§2.44) (standard reference, not scraped)
Stanford Math 205A, Homework 1 (standard reference, not scraped)
University of Chicago MATH 395 notes (standard reference, not scraped)

The Cantor set is exactly the set of ∑k≥1ak3−k∑k≥1​ak​3−k with every ak∈{0,2}ak​∈{0,2}, and this gives a bijection with {0,1}N{0,1}N