Alphabeta Math
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.

For ∣r∣<1, ∑k≥0rk=1/(1−r), and for ∣r∣≥1 the series diverges

Statement

Let r∈R and let rk be the integer power (Integer powers am), so that r0=1 for every r, including r=0.

  1. If ∣r∣<1 then the series ∑rk converges (Series, partial sums, convergence and the sum, divergence, and the tail series) and ∑k=0∞rk  =  11−r.
  2. If ∣r∣≥1 then ∑rk diverges.

The series starts at k=0 and its first term is r0=1; in particular ∑k=0∞2−k=2, while the series starting at k=1 sums to 1. Which starting index is meant has to be said, and it is said here.

Facts & Assumptions

Given: A real number r, the integer powers rk (Integer powers am), and the partial sums sn=∑k<nrk of ∑rk (Series, partial sums, convergence and the sum, divergence, and the tail series, Finite sums and finite products, by recursion).

[L1]

Factorisation of a difference of powers: for a,b∈R and natural n≥1, bn−an=(b−a)∑k=0n−1akb n−1−k (Factorisation of bn−an, and the resulting Lipschitz estimate).

[L3]

Algebra of limits: sums, differences and quotients of convergent sequences converge to the corresponding combination, the quotient rule requiring a nonzero limit and nonzero denominators (Algebra of limits: sums, scalar multiples, products and quotients, Limits and Cauchy sequences of reals).

[L4]

Absolute value: ∣xy∣=∣x∣ ∣y∣, ∣x∣≥0, and ∣x∣=0 exactly when x=0; also ∣1∣=1, since 1>0 (Basic properties of the absolute value).

[L5]

Powers and order: a0=1 for every a; if a≥1 and n≥1 then an≥a≥1; and 1n=1 for every n (Monotonicity of x↦xn and of n↦an, Integer powers am).

[L6]

The principle of induction (The principle of mathematical induction).

[L7]

If a series converges then its terms tend to 0 (If a series converges then its terms tend to 0).

[L8]

Notation of Finite sums and finite products, by recursion: ∑k=0n−1xk is ∑k<nxk, and the empty sum ∑k<0xk is 0.

Proof

technique · cases
1.1

Assume ∣r∣<1.

assume-case lt
1.2

Assume instead ∣r∣≥1.

assume-case ge
1.3

For every natural n≥1, applying [L1] with b=1 and a=r gives 1−rn=(1−r)∑k=0n−1rk⋅1 n−1−k=(1−r) sn, using 1m=1 and the notation of [L8].

L1L5L8
1.4

At n=0 the identity 1−rn=(1−r)sn also holds, both sides being 0 because r0=1 and s0 is the empty sum.

L5L8
2.1

In the case ∣r∣<1 we have r≠1, since ∣1∣=1 and ∣r∣<1; hence 1−r≠0.

step 1.1L4algebra
2.2

In the case ∣r∣≥1, an induction gives ∣rk∣=∣r∣k for every k∈N: at k=0 both sides are 1, and if ∣rk∣=∣r∣k then ∣rk+1∣=∣rk⋅r∣=∣rk∣ ∣r∣=∣r∣k∣r∣=∣r∣k+1.

step 1.2L4L5L6
2.3

In the case ∣r∣≥1 we get ∣r∣k≥1 for every k∈N: at k=0 this reads 1≥1, and for k≥1 it is the comparison ∣r∣k≥∣r∣≥1.

step 1.2L5
3.1

In the case ∣r∣<1, dividing by 1−r≠0 gives sn=(1−rn)/(1−r) for every n∈N.

step 2.1step 1.3step 1.4algebra
3.2

In the case ∣r∣≥1, combining the two previous steps gives ∣rk−0∣=∣rk∣=∣r∣k≥1 for every k∈N.

step 2.2step 2.3
4.1

In the case ∣r∣<1 the sequence (rn) is null, so 1−rn→1 and therefore sn→1/(1−r), the denominator being the nonzero constant 1−r; hence ∑rk converges with sum 1/(1−r), which is claim 1.

step 1.1step 3.1step 2.1L2L3
4.2

In the case ∣r∣≥1 the sequence (rk) does not converge to 0, since the rational tolerance ε=1 admits no index K with ∣rk−0∣<1 for all k≥K; so by the term test ∑rk diverges, which is claim 2.

step 3.2L7
5.1

The two cases ∣r∣<1 and ∣r∣≥1 exhaust the possibilities, since the order on R is total, so claims 1 and 2 together cover every real r.

step 4.1step 4.2cases-exhaustive∎

Remarks

  • The divergence half needs no separate treatment of r=1 and r=−1. Both are covered by ∣r∣≥1, and the single reason is the same in every case: the terms have absolute value at least 1, so they cannot tend to 0. For r=1 the partial sums are sn=n and run to +∞; for r=−1 they oscillate between 0 and 1. The theorem says only that neither converges, which is all that "diverges" means here (Series, partial sums, convergence and the sum, divergence, and the tail series).

  • Why the identity is proved at n=0 separately. Factorisation of bn−an, and the resulting Lipschitz estimate requires n≥1, since its right-hand side is a sum over k<n of a term involving b n−1−k, and n−1 is not a natural number at n=0. The identity is still true at n=0, but by inspection of two empty objects rather than by that lemma, and step 1.4 says so rather than letting the reader assume the citation covers it.

Depends on

Used by

…and 64 more results.

Dependency tree · two levels

56 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