TheoremStatement: Literature-sourcedProof: 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.

Base- $b$ expansions: for an integer $b \geq 2$ every $x \in [0, 1)$ is the sum of $\sum_{j \geq 0} d_{j} / b^{j + 1}$ for digits $d_{j} < b$ , and the digit sequence is unique among those that are not eventually constantly $b - 1$

Statement

Let $b \in N$ with $b \geq 2$ and write $β : = ι (b)$ for the canonical natural of $b$ in $R$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field), so that $β > 1$ (Canonical naturals are positive and strictly increasing); powers $β^{n}$ are integer powers (Integer powers $a^{m}$ ). Call a sequence $(d_{j})$ of natural numbers a digit sequence in base $b$ when $d_{j} < b$ for every $j$ , and say it is terminal when it is eventually constantly $b - 1$ , that is when there is $J$ with $d_{j} = b - 1$ for every $j \geq J$ . Then:

Existence. For every $x \in [0, 1)$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) there is a non-terminal digit sequence $(d_{j})$ in base $b$ with $\sum_{j \geq 0} \frac{ι (d_{j})}{β^{j + 1}} convergent, of sum x .$
Uniqueness. If $(c_{j})$ and $(c_{j}^{'})$ are non-terminal digit sequences in base $b$ whose series have the same sum, then $c_{j} = c_{j}^{'}$ for every $j$ .

So every real in $[0, 1)$ has exactly one base- $b$ expansion once the terminal sequences are excluded. The assignment $x \mapsto (d_{j})$ is moreover a bijection onto the non-terminal digit sequences: claim 2 makes it injective, and it is onto because a non-terminal $(c_{j})$ has $ι (c_{j}) \leq β - 1$ for every $j$ and $ι (c_{j}) < β - 1$ for infinitely many $j$ , so its sum is strictly below the sum $1$ of the all- $(b - 1)$ series computed in step 8.1, hence lies in $[0, 1)$ and has $(c_{j})$ as its expansion by claim 2. Excluding them is unavoidable: the terminal sequences are exactly the ones producing a second expansion of a number that already has one, as the companion examples page exhibits with $0.999 \dots = 1$ and $0.4999 \dots = 0.5$ .

The construction uses no floor function. The integer part of a real is not available at this point in the reading order, so the digit at each stage is produced by the finite case distinction "in which of the $b$ intervals $[d / β, (d + 1) / β)$ does the current residue lie", closed by the well-ordering principle (The well-ordering principle), and the digits are assembled by the recursion theorem (The recursion theorem).

Indices run from $0$ . The digit $d_{j}$ carries the weight $β^{- (j + 1)}$ , so that the first digit has weight $1 / β$ and no denominator $β^{0} = 1$ ever occurs.

Facts & Assumptions

Given: A natural number $b \geq 2$ , $β = ι (b)$ , and a real $x \in [0, 1)$ .

[L1]

The canonical natural: $ι (0) = 0$ , $ι (n + 1) = ι (n) + 1$ , $ι$ is strictly increasing on $N$ , and $ι (m + n) = ι (m) + ι (n)$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing).

[L2]

Integer powers: $β^{0} = 1$ , $β^{n + 1} = β^{n} β$ , $(u v)^{n} = u^{n} v^{n}$ , and $β^{n} > 0$ for $β > 0$ (Integer powers $a^{m}$ , Laws of integer exponents).

[L3]

$[0, 1) = {y \in R : 0 \leq y < 1}$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L4]

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

[L5]

The recursion theorem (The recursion theorem) and the principle of induction (The principle of mathematical induction).

[L6]

Geometric series: for $∣ r ∣ < 1$ , $\sum r^{k}$ converges with sum $1 / (1 - r)$ ; and the terms of a convergent series tend to $0$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges, If a series converges then its terms tend to $0$ ).

[L7]

Order and inverses: $0 < u < v$ implies $0 < 1 / v < 1 / u$ (Inverses of positives are positive, and reciprocation reverses order).

[L8]

Finite sums: recursion, splitting, additivity, scaling and monotonicity; in particular every single term of a finite sum of nonnegative reals is at most that sum (Laws of finite sums and finite products).

[L9]

Partial sums and sums of series; linearity of convergent series; and a series converges if and only if some tail series converges, the sum being the initial partial sum plus the tail sum (Series, partial sums, convergence and the sum, divergence, and the tail series, Convergent series add and scale termwise, A series converges iff each of its tail series converges, and the sum splits as $s_{N}$ plus the $N$ -th tail, Limits and Cauchy sequences of reals).

[L10]

For a series of nonnegative terms, every partial sum is at most the sum (A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum).

[L11]

The squeeze theorem, the algebra of limits, and that limits preserve non-strict inequalities (The squeeze theorem, Algebra of limits: sums, scalar multiples, products and quotients, Limits preserve non-strict inequalities).

Proof

technique · constructive

1.1

$β = ι (b) \geq ι (2) = 1 + 1 > 1 > 0$ , and an induction gives $β^{n} > 0$ for every $n$ ; also $0 < 1 / β < 1$ .

givenL1L2L5L7

1.2

For uniqueness, let $(c_{j})$ and $(c_{j}^{'})$ be non-terminal digit sequences whose series have the same sum, and suppose they are not equal. By [L4] let $n$ be least with $c_{n} \neq c_{n}^{'}$ ; interchanging the two sequences if necessary, assume $c_{n} < c_{n}^{'}$ , so $ι (c_{n}^{'}) - ι (c_{n}) \geq 1$ .

givenL1L4choose

2.1

The digit of a residue. For every $r \in [0, 1)$ there is exactly one natural $d < b$ with $ι (d) / β \leq r < ι (d + 1) / β$ . For existence, the set $D : = {d \in N : d \leq b and r < ι (d) / β}$ contains $b$ , since $ι (b) / β = 1 > r$ ; let $m : = \min D$ , which is not $0$ because $ι (0) / β = 0 \leq r$ ; put $d : = m - 1$ , so $d < b$ , and minimality of $m$ says $d \notin D$ , that is $ι (d) / β \leq r$ , while $m \in D$ says $r < ι (m) / β = ι (d + 1) / β$ . For uniqueness, if $d < d^{'}$ both worked then $r < ι (d + 1) / β \leq ι (d^{'}) / β \leq r$ , which the order forbids. Write $d (r)$ for this digit.

step 1.1L1L3L4construct

2.2

Both series converge, by hypothesis, so by linearity $\sum_{j} (ι (c_{j}^{'}) - ι (c_{j})) / β^{j + 1}$ converges with sum $0$ ; its first $n$ terms vanish, so by [L9] the tail from $n$ also has sum $0$ , that is $0 = (ι (c_{n}^{'}) - ι (c_{n})) / β^{n + 1} + \sum_{j > n} (ι (c_{j}^{'}) - ι (c_{j})) / β^{j + 1}$ .

givenstep 1.2L9

3.1

The residue map. For $r \in [0, 1)$ put $f (r) : = β r - ι (d (r))$ . Multiplying $ι (d (r)) / β \leq r < ι (d (r) + 1) / β = (ι (d (r)) + 1) / β$ by $β > 0$ gives $ι (d (r)) \leq β r < ι (d (r)) + 1$ , so $0 \leq f (r) < 1$ ; thus $f$ is a function from $[0, 1)$ to $[0, 1)$ .

step 1.1step 2.1L1L3construct

3.2

Every difference satisfies $ι (c_{j}^{'}) - ι (c_{j}) \geq - (β - 1)$ , the digits lying in ${0, \dots, b - 1}$ , and $\sum_{j > n} (β - 1) / β^{j + 1} = \frac{β - 1}{β^{n + 2}} \cdot \frac{1}{1 - 1 / β} = \frac{1}{β^{n + 1}}$ by the geometric series; hence the tail in step 2.2 is at least $- 1 / β^{n + 1}$ .

step 1.2L1L2L6L11

4.1

By the recursion theorem applied to the set $[0, 1)$ , the element $x$ and the function $f$ , there is a unique sequence $(r_{n})$ in $[0, 1)$ with $r_{0} = x$ and $r_{n + 1} = f (r_{n})$ ; put $d_{j} : = d (r_{j})$ , a natural number $< b$ , so $(d_{j})$ is a digit sequence in base $b$ .

step 3.1L5construct

4.2

Write $A$ for the first summand and $B$ for the tail in step 2.2, so $A + B = 0$ while $A \geq 1 / β^{n + 1}$ by step 1.2 and $B \geq - 1 / β^{n + 1}$ by step 3.2; since the two lower bounds sum to $0$ , both must be attained, that is $A = 1 / β^{n + 1}$ and $B = - 1 / β^{n + 1}$ ; in particular $\sum_{j > n} (ι (c_{j}^{'}) - ι (c_{j}) + (β - 1)) / β^{j + 1} = 0$ , a convergent series of nonnegative terms with sum $0$ , so every term is $0$ and $ι (c_{j}^{'}) - ι (c_{j}) = - (β - 1)$ for every $j > n$ .

step 1.2step 2.2step 3.2L8L9L10

5.1

An induction gives $x = \sum_{j < n} ι (d_{j}) / β^{j + 1} + r_{n} / β^{n}$ for every $n$ : at $n = 0$ the sum is empty and $r_{0} / β^{0} = x$ ; and from $r_{n} = (ι (d_{n}) + r_{n + 1}) / β$ , which is step 3.1 rearranged, one gets $r_{n} / β^{n} = ι (d_{n}) / β^{n + 1} + r_{n + 1} / β^{n + 1}$ .

step 3.1step 4.1L2L5L8

5.2

Since $0 \leq r_{n} < 1$ and $β^{n} > 0$ , we have $0 \leq r_{n} / β^{n} \leq 1 / β^{n} = (1 / β)^{n}$ ; as $0 < 1 / β < 1$ the series $\sum (1 / β)^{k}$ converges, so $(1 / β)^{n} \to 0$ , and the squeeze gives $r_{n} / β^{n} \to 0$ .

step 1.1step 4.1L2L6L7L11

5.3

That forces $c_{j} = b - 1$ and $c_{j}^{'} = 0$ for every $j > n$ , since the difference of two digits attains $- (β - 1)$ only at those values; so $(c_{j})$ is terminal, contrary to hypothesis. Hence the two digit sequences agree, which is claim 2.

step 1.2step 4.2L1

6.1

By step 5.1 the partial sums of $\sum_{j} ι (d_{j}) / β^{j + 1}$ equal $x - r_{n} / β^{n}$ , which converges to $x$ ; so the series converges with sum $x$ .

step 5.1step 5.2L9L11

7.1

Applying step 5.1 and step 6.1 to the residue $r_{J}$ in place of $x$ , whose recursion produces the digits $d_{J + i}$ , gives $r_{J} = \sum_{i \geq 0} ι (d_{J + i}) / β^{i + 1}$ for every $J$ .

step 4.1step 6.1L5

8.1

The constructed sequence is not terminal: if $d_{j} = b - 1$ for every $j \geq J$ , then by step 7.1 and the geometric series, $r_{J} = \sum_{i \geq 0} (β - 1) / β^{i + 1} = \frac{β - 1}{β} \cdot \frac{1}{1 - 1 / β} = 1$ , contradicting $r_{J} < 1$ ; here $ι (b - 1) = β - 1$ by [L1]. With step 6.1 this proves claim 1.

step 6.1step 7.1L1L2L6L9

9.1

Claim 1 is step 6.1 with step 8.1 and claim 2 is step 5.3, so every $x \in [0, 1)$ has exactly one non-terminal base- $b$ expansion.

step 6.1step 8.1step 5.3discharge-construct∎

Remarks

Where each tool is used, and the floor function is not among them. The well-ordering principle appears once, in step 2.1, to pick out the digit from the finitely many candidates $0, \dots, b$ ; the recursion theorem appears once, in step 4.1, to turn the one-step residue map into a sequence. Everything else is the geometric series and the ordering of $R$ . The usual formula $d_{n} = ⌊ β r_{n} ⌋$ would need the integer part of a real, which is developed later in the reading order.
The exclusion of terminal sequences is exactly one equivalence class. Step 4.2 shows that two distinct expansions of the same number must differ by one at the first place where they differ and then be all $b - 1$ against all $0$ . So each real in $(0, 1)$ whose expansion terminates in zeros has exactly two expansions and every other real exactly one; forbidding the all- $(b - 1)$ tails picks one from each pair.
The hypothesis $x < 1$ is not a restriction on the theorem so much as on the notation. The all- $(b - 1)$ sequence sums to $1$ , as step 8.1 computes, and $1$ is not in $[0, 1)$ ; a base- $b$ expansion of a general nonnegative real is an integer part together with an expansion of the fractional part, and the integer part is not available here.

Depends on

Used by

Dependency tree · two levels

69 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

Decimal representation (Wikipedia) (standard reference, not scraped)
Positional notation (Wikipedia) (standard reference, not scraped)
M365C Real Analysis (standard reference, not scraped)

Base-bb expansions: for an integer b≥2b≥2 every x∈[0,1)x∈[0,1) is the sum of ∑j≥0dj/b j+1∑j≥0​dj​/bj+1 for digits dj<bdj​<b, and the digit sequence is unique among those that are not eventually constantly b−1b−1