Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

∑(bk−bk+1)\sum (b_k - b_{k+1}) converges iff (bk)(b_k) converges, with sum b0−lim⁡bkb_0 - \lim b_k

Statement

Let (bk)(b_k) be a sequence of reals and put ak:=bk−bk+1a_k := b_k - b_{k+1}. Then the partial sums of ∑ak\sum a_k are

sn  =  ∑k<n(bk−bk+1)  =  b0−bn(n∈N),s_n \;=\; \sum_{k<n} (b_k - b_{k+1}) \;=\; b_0 - b_n \qquad (n \in \mathbb{N}),

and consequently ∑ak\sum a_k converges (Series, partial sums, convergence and the sum, divergence, and the tail series) if and only if (bk)(b_k) converges (Limits and Cauchy sequences of reals), in which case

∑k=0∞(bk−bk+1)  =  b0−lim⁡kbk.\sum_{k=0}^{\infty} (b_k - b_{k+1}) \;=\; b_0 - \lim_{k} b_k .

For a family from a general starting index mm the same statement holds with b0b_0 replaced by bmb_m, being this statement applied to the shifted sequence j↦bj+mj \mapsto b_{j+m} (Series, partial sums, convergence and the sum, divergence, and the tail series).

Facts & Assumptions

Given: A sequence (bk)(b_k) of reals, the sequence ak:=bk−bk+1a_k := b_k - b_{k+1}, and the partial sums sn=∑k<naks_n = \sum_{k<n} a_k (Series, partial sums, convergence and the sum, divergence, and the tail series, Finite sums and finite products, by recursion).

[L1]

Telescoping of finite sums: ∑k<n(ck+1−ck)=cn−c0\sum_{k<n}(c_{k+1} - c_k) = c_n - c_0 for every sequence (ck)(c_k) of reals and every n∈Nn \in \mathbb{N} (Laws of finite sums and finite products).

[L2]

Algebra of limits: if xn→xx_n \to x and yn→yy_n \to y then xn−yn→x−yx_n - y_n \to x - y (Algebra of limits: sums, scalar multiples, products and quotients).

[L3]

A constant sequence with value cc converges to cc (Limits and Cauchy sequences of reals).

Proof

technique · direct
1.1

Apply [L1] to the sequence ck:=−bkc_k := -b_k: it gives ∑k<n(−bk+1−(−bk))=−bn−(−b0)\sum_{k<n}(-b_{k+1} - (-b_k)) = -b_n - (-b_0), that is ∑k<n(bk−bk+1)=b0−bn\sum_{k<n}(b_k - b_{k+1}) = b_0 - b_n.

L1algebra
2.1

So sn=b0−bns_n = b_0 - b_n for every n∈Nn \in \mathbb{N}, and equivalently bn=b0−snb_n = b_0 - s_n.

step 1.1algebra
3.1

Suppose (bk)(b_k) converges, say bn→Bb_n \to B; then sn=b0−bn→b0−Bs_n = b_0 - b_n \to b_0 - B, so ∑ak\sum a_k converges with sum b0−Bb_0 - B.

step 2.1L2L3
3.2

Suppose conversely that ∑ak\sum a_k converges, say sn→Ss_n \to S; then bn=b0−sn→b0−Sb_n = b_0 - s_n \to b_0 - S, so (bk)(b_k) converges.

step 2.1L2L3
4.1

The two implications give the stated equivalence, and in the convergent case step 3.1 gives the sum b0−lim⁡kbkb_0 - \lim_k b_k.

step 3.1step 3.2∎

Remarks

  • The first term of (bk)(b_k) survives and the rest cancel. That is the whole content, and it is where an off-by-one error is easiest to make: the sum is b0−lim⁡bkb_0 - \lim b_k and not b1−lim⁡bkb_1 - \lim b_k, because the partial sum sn=∑k<ns_n = \sum_{k<n} starts at k=0k = 0 (Series, partial sums, convergence and the sum, divergence, and the tail series). A series written from k=1k = 1 telescopes to b1−lim⁡bkb_1 - \lim b_k instead.

  • No sign or monotonicity hypothesis is used. The lemma is an identity between finite sums followed by one limit rule, so it applies to sequences (bk)(b_k) of any sign and is not restricted to the decreasing case in which telescoping series usually appear.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 62 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources