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

A series converges iff for every $\varepsilon > 0$ there is $N$ with $|a_{m+1} + \dots + a_n| < \varepsilon$ for all $n > m \ge N$

Statement

Let $(a_k)$ be a sequence of reals, with partial sums $s_n = \sum_{k<n} a_k$ (Series, partial sums, convergence and the sum, divergence, and the tail series). Then $\sum a_k$ converges if and only if

$\text{for every real } \varepsilon > 0 \text{ there is } N \in \mathbb{N} \text{ such that } \Big| \sum_{k=m+1}^{n} a_k \Big| < \varepsilon \text{ for all } n > m \ge N .$

The block $\sum_{k=m+1}^{n} a_k$ is the finite sum $a_{m+1} + \dots + a_n$ of Finite sums and finite products, by recursion, and it equals $s_{n+1} - s_{m+1}$ .

This is the Cauchy criterion transported from sequences to series. Its value is that it decides convergence without producing, or even naming, the sum.

Facts & Assumptions

Given: A sequence $(a_k)$ of reals with partial sums $s_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]

Splitting of finite sums: if $m' \le n'$ then $\sum_{k<n'} a_k = \sum_{k<m'} a_k + \sum_{k=m'}^{n'-1} a_k$ (Laws of finite sums and finite products, Finite sums and finite products, by recursion).

[L2]

Every convergent sequence of reals is Cauchy (Every convergent sequence is Cauchy).

[L3]

Every Cauchy sequence of reals converges (The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges).

[L4]

Cauchyness reads: for every rational $\varepsilon > 0$ there is $K$ with $|s_p - s_q| < \varepsilon$ for all $p, q \ge K$ (Limits and Cauchy sequences of reals). Rational and real tolerances give the same condition, because every real $\varepsilon > 0$ exceeds some rational $1/n$ with $n \ge 1$ natural (For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$ ), and conversely every positive rational is a positive real.

Proof

technique · direct

1.1

For all naturals $m < n$ , splitting $s_{n+1}$ at the index $m+1 \le n+1$ gives $s_{n+1} = s_{m+1} + \sum_{k=m+1}^{n} a_k$ , hence $\sum_{k=m+1}^{n} a_k = s_{n+1} - s_{m+1}$ .

L1algebra

1.2

Conversely, every pair $p > q \ge 1$ of naturals is of the form $p = n+1$ , $q = m+1$ with $n = p - 1 > m = q - 1 \ge 0$ .

givenalgebra

1.3

Suppose $\sum a_k$ converges, that is $(s_n)$ converges; then $(s_n)$ is Cauchy.

givenL2

1.4

Suppose conversely that the stated condition holds, and let a rational $\varepsilon > 0$ be given; take $N$ for $\varepsilon$ as in the condition and put $K := N + 1$ .

givenchoose

2.1

Let a real $\varepsilon > 0$ be given, choose a rational $\varepsilon'$ with $0 < \varepsilon' < \varepsilon$ , and take $K$ for $\varepsilon'$ as in the Cauchy condition; put $N := K$ .

step 1.3L4choose

2.2

Let $p, q \ge K$ . If $p = q$ then $|s_p - s_q| = 0 < \varepsilon$ ; otherwise one of them exceeds the other, and by symmetry we may take $p > q \ge K \ge 1$ .

step 1.4algebra

3.1

For all $n > m \ge N$ one has $n + 1 > m + 1 \ge K$ , so $\big|\sum_{k=m+1}^{n} a_k\big| = |s_{n+1} - s_{m+1}| < \varepsilon' < \varepsilon$ , which is the stated condition.

step 2.1step 1.1L4

3.2

Writing $p = n+1$ and $q = m+1$ gives $n > m$ and $m = q - 1 \ge K - 1 = N$ , so the condition applies and $|s_p - s_q| = \big|\sum_{k=m+1}^{n} a_k\big| < \varepsilon$ .

step 2.2step 1.2step 1.1step 1.4

4.1

So $(s_n)$ is Cauchy, hence converges, hence $\sum a_k$ converges.

step 2.2step 3.2L4L3

5.1

The two implications together are the stated equivalence.

step 3.1step 4.1∎

Remarks

The criterion is stated over blocks, not over partial sums, on purpose. In applications one estimates a run of consecutive terms $a_{m+1}, \dots, a_n$ directly; the translation into $|s_{n+1} - s_{m+1}|$ is step 1.1 and is done once here so that no later proof has to repeat it.
Taking $n = m+1$ recovers the term test. The single-term block gives $|a_{m+1}| < \varepsilon$ for all $m \ge N$ , which is $a_k \to 0$ ; so If a series converges then its terms tend to $0$ is the weakest consequence of this criterion. The criterion is strictly stronger, since it constrains arbitrarily long blocks and not only single terms.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 76 results over 24 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

Cauchy's convergence test (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (standard reference, not scraped)
John K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)

A series converges iff for every ε>0\varepsilon > 0ε>0 there is NNN with ∣am+1+⋯+an∣<ε|a_{m+1} + \dots + a_n| < \varepsilon∣am+1​+⋯+an​∣<ε for all n>m≥Nn > m \ge Nn>m≥N