Alphabeta Math
ExampleConstruction: AI-adaptedVerification: 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.

0.999⋯=1 and 0.4999⋯=0.5: the second expansion of a number is exactly an eventually-all-(b−1) digit sequence

Example

Take b=10, so β=ι(10), and read a digit sequence (dj) as the series ∑j≥0ι(dj)/β j+1 (Base-b expansions: for an integer b≥2 every x∈[0,1) is the sum of ∑j≥0dj/b j+1 for digits dj<b, and the digit sequence is unique among those that are not eventually constantly b−1).

All nines. The constant sequence dj=9 gives, by the geometric series,

∑j≥0910 j+1  =  910⋅11−1/10  =  1,

which is the statement usually written 0.999⋯=1. Since 1∉[0,1) (Intervals of R: the nine order-convex forms, nondegeneracy, and length), this digit sequence is not the expansion of any point of [0,1) produced by Base-b expansions: for an integer b≥2 every x∈[0,1) is the sum of ∑j≥0dj/b j+1 for digits dj<b, and the digit sequence is unique among those that are not eventually constantly b−1, and no uniqueness clause is violated.

Two expansions of one number. For x=1/2 the construction of Base-b expansions: for an integer b≥2 every x∈[0,1) is the sum of ∑j≥0dj/b j+1 for digits dj<b, and the digit sequence is unique among those that are not eventually constantly b−1 returns d0=5 and dj=0 for j≥1: the residue r0=1/2 lies in [5/10,6/10), and r1=10⋅12−5=0, after which every digit is 0. But the sequence d0′=4, dj′=9 for j≥1 has

410+∑j≥1910 j+1  =  410+9100⋅11−1/10  =  410+110  =  12,

which is 0.4999⋯=0.5. So two different digit sequences have the same sum, and uniqueness in Base-b expansions: for an integer b≥2 every x∈[0,1) is the sum of ∑j≥0dj/b j+1 for digits dj<b, and the digit sequence is unique among those that are not eventually constantly b−1 survives only because (dj′) is terminal, being eventually constantly b−1=9.

This is the whole of the nonuniqueness. The uniqueness proof shows that two distinct digit sequences with the same sum must differ by one at the first index where they differ and then be all b−1 against all 0. So excluding the terminal sequences excludes exactly one member of each such pair, and nothing else.

Facts & Assumptions

Given: The base b=10 with β=ι(10), the digit sequences dj=9 for all j; e0=5 with ej=0 for j≥1; and d0′=4 with dj′=9 for j≥1.

[L1]

Geometric series: for ∣x∣<1, ∑kxk converges with sum 1/(1−x), the first term being x0=1 (For ∣r∣<1, ∑k≥0rk=1/(1−r), and for ∣r∣≥1 the series diverges, Series, partial sums, convergence and the sum, divergence, and the tail series).

[L2]

Powers and canonical naturals: β0=1, βn+1=βnβ, (uv)n=unvn; ι is additive and multiplicative on positive naturals and strictly increasing (Integer powers am, Laws of integer exponents, The canonical natural ι(n)=n⋅1F of a field, Canonical naturals are positive and strictly increasing).

[L3]

Linearity of convergent series, and a series converges if and only if each tail series does, the sum splitting as the initial partial sum plus the tail sum (Convergent series add and scale termwise, A series converges iff each of its tail series converges, and the sum splits as sN plus the N-th tail, Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L4]

Base-b expansions: for b≥2 every x∈[0,1) has exactly one non-terminal digit sequence summing to x, the digits being produced by the residue recursion with d(r) the unique digit with ι(d)/β≤r<ι(d+1)/β (Base-b expansions: for an integer b≥2 every x∈[0,1) is the sum of ∑j≥0dj/b j+1 for digits dj<b, and the digit sequence is unique among those that are not eventually constantly b−1, Intervals of R: the nine order-convex forms, nondegeneracy, and length, Limits and Cauchy sequences of reals).

Verification

technique · direct
1.1

Since β=ι(10)≥2>1, one has 0<1/β<1, so ∑k(1/β)k converges with sum 1/(1−1/β)=β/(β−1)=10/9.

L1L2
1.2

For x=1/2 the residue recursion gives d0=5, since ι(5)/β=1/2≤1/2<6/10=ι(6)/β, and then r1=β⋅12−ι(5)=5−5=0, whence dj=0 and rj+1=0 for every j≥1. This sequence is non-terminal and sums to 5/10=1/2.

L2L4
2.1

Hence ∑j≥09/β j+1=(9/β)∑j≥0(1/β) j=(9/10)(10/9)=1, using linearity and β j+1=β β j.

step 1.1L2L3
3.1

So the all-nines digit sequence has sum 1, and 1∉[0,1); by [L4] it is therefore not the expansion of any x∈[0,1), and it is terminal.

step 2.1L4
3.2

The sequence (dj′) with d0′=4 and dj′=9 for j≥1 has sum 4/10+∑j≥19/β j+1, and by step 2.1 with the first term removed, ∑j≥19/β j+1=(1/β)∑j≥09/β j+1=1/10; so its sum is 4/10+1/10=1/2.

step 2.1L2L3
4.1

Thus (ej) and (dj′) are different digit sequences with the same sum 1/2, so a real number in [0,1) can have two base-10 expansions.

step 1.2step 3.2
5.1

No uniqueness claim is contradicted: (dj′) is terminal, being constantly 9=b−1 from index 1 on, and [L4] asserts uniqueness only among non-terminal sequences, of which (ej) is the one belonging to 1/2.

step 1.2step 4.1L4∎

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

49 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