Alphabeta Math
LemmaStatement: Literature-sourcedProof: 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.

If a series converges then its terms tend to 00

Statement

Let (ak)(a_k) be a sequence of reals. If the series ak\sum a_k converges (Series, partial sums, convergence and the sum, divergence, and the tail series) then the sequence (ak)(a_k) converges (Limits and Cauchy sequences of reals), with

limkak  =  0.\lim_{k} a_k \;=\; 0 .

Equivalently, in the contrapositive form in which the lemma is almost always used: if (ak)(a_k) does not converge to 00 then ak\sum a_k diverges.

The same statement holds for a series kmak\sum_{k \ge m} a_k with a general starting index, with the conclusion that (aj+m)jN(a_{j+m})_{j \in \mathbb{N}} converges to 00: that series is by definition the series of the sequence bj=aj+mb_j = a_{j+m} (Series, partial sums, convergence and the sum, divergence, and the tail series), so it is the statement above applied to (bj)(b_j).

The converse is false; it is refuted by FALSE: if ak0a_k \to 0 then ak\sum a_k converges.

Facts & Assumptions

Given: A sequence (ak)(a_k) of reals whose series converges, with 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]

The recursion clause of the finite sum: sn+1=sn+ans_{n+1} = s_n + a_n for every nNn \in \mathbb{N} (Finite sums and finite products, by recursion, Series, partial sums, convergence and the sum, divergence, and the tail series).

[L2]

Convergence depends only on the tail: if (xn)(x_n) converges to xx then so does its 11-st tail (xn+1)n(x_{n+1})_{n} (Convergence depends only on the tail, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L3]

Algebra of limits: if xnxx_n \to x and ynyy_n \to y then xnynxyx_n - y_n \to x - y (Algebra of limits: sums, scalar multiples, products and quotients).

Proof

technique · direct
1.1

The sequence (sn+1)nN(s_{n+1})_{n \in \mathbb{N}} is the 11-st tail of (sn)(s_n), and it converges to SS.

A1L2
1.2

From the recursion clause, an=sn+1sna_n = s_{n+1} - s_n for every nNn \in \mathbb{N}.

L1algebra
2.1

Hence (an)(a_n) is the difference of two sequences converging to SS, so it converges to SS=0S - S = 0.

step 1.1step 1.2A1L3
3.1

That is the claim, and its contrapositive is the assertion that a series whose terms do not tend to 00 diverges.

step 2.1

Remarks

  • This is a necessary condition and never a sufficient one. It rules a series out; it never rules one in. The harmonic series has terms tending to 00 and diverges, which is exactly the content of FALSE: if ak0a_k \to 0 then ak\sum a_k converges.

  • What the proof actually uses. Only that the partial sums converge and that consecutive partial sums differ by a term. No sign hypothesis is placed on (ak)(a_k), and none is available at this point on the page.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 64 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