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

Grouping: if ∑ak\sum a_k converges and (nj)(n_j) is strictly increasing with n0=0n_0 = 0, the series of blocks ∑k=njnj+1−1ak\sum_{k=n_j}^{n_{j+1}-1} a_k converges to the same sum

Statement

Let (ak)(a_k) be a sequence of reals whose series converges (Series, partial sums, convergence and the sum, divergence, and the tail series), with sum SS, and let n:N→Nn : \mathbb{N} \to \mathbb{N} be strictly increasing (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences) with n0=0n_0 = 0. Define the blocks

Bj  :=  ∑k=njnj+1−1ak(j∈N),B_j \;:=\; \sum_{k = n_j}^{n_{j+1}-1} a_k \qquad (j \in \mathbb{N}),

each a finite sum of nj+1−nj≥1n_{j+1} - n_j \ge 1 consecutive terms (Finite sums and finite products, by recursion). Then ∑Bj\sum B_j converges, with

∑j=0∞Bj  =  S.\sum_{j=0}^{\infty} B_j \;=\; S .

The proof shows more, and the extra is what makes the theorem trivial once seen: the mm-th partial sum of ∑Bj\sum B_j is exactly snms_{n_m}, the nmn_m-th partial sum of ∑ak\sum a_k. Grouping does not produce a new series so much as a subsequence of the old partial sums.

The converse fails. A grouped series may converge while the original diverges, and FALSE: if some grouping of a series converges then the series itself converges records that, with the witness on the companion page. What the theorem needs is convergence of ∑ak\sum a_k as a hypothesis, and n0=0n_0 = 0, without which the first block would omit the terms before n0n_0.

Facts & Assumptions

Given: A sequence (ak)(a_k) of reals with ∑ak\sum a_k convergent of sum SS and partial sums sn=∑k<naks_n = \sum_{k<n} a_k; a strictly increasing n:N→Nn : \mathbb{N} \to \mathbb{N} with n0=0n_0 = 0; and the blocks Bj=∑k=njnj+1−1akB_j = \sum_{k=n_j}^{n_{j+1}-1} a_k.

[L1]

Finite sums: ∑k<0xk=0\sum_{k<0} x_k = 0 and ∑k<m+1xk=∑k<mxk+xm\sum_{k<m+1} x_k = \sum_{k<m} x_k + x_m (Finite sums and finite products, by recursion).

[L2]

Splitting: if m≤nm \le n then ∑k<nak=∑k<mak+∑k=mn−1ak\sum_{k<n} a_k = \sum_{k<m} a_k + \sum_{k=m}^{n-1} a_k (Laws of finite sums and finite products).

[L3]

The partial sums of a series and the meaning of its sum (Series, partial sums, convergence and the sum, divergence, and the tail series, Limits and Cauchy sequences of reals).

[L4]

A subsequence of a convergent sequence converges to the same limit; a subsequence is indexed by a strictly increasing map N→N\mathbb{N} \to \mathbb{N} (Subsequences inherit the limit, Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences).

[L5]

The principle of induction on N\mathbb{N} (The principle of mathematical induction).

Proof

technique · direct
1.1

Since nn is strictly increasing, nj<nj+1n_j < n_{j+1} for every jj, so each block BjB_j is a finite sum over a nonempty range of indices and is a well-determined real.

givenL1L2
1.2

The map m↦nmm \mapsto n_m is strictly increasing, so (snm)m(s_{n_m})_m is a subsequence of the convergent sequence (sn)(s_n) and therefore converges to SS.

givenL3L4
2.1

An induction on mm gives ∑j<mBj=snm\sum_{j<m} B_j = s_{n_m} for every m∈Nm \in \mathbb{N}: at m=0m = 0 the left side is the empty sum 00 and the right side is sn0=s0=0s_{n_0} = s_0 = 0; and if ∑j<mBj=snm\sum_{j<m} B_j = s_{n_m} then ∑j<m+1Bj=snm+Bm=∑k<nmak+∑k=nmnm+1−1ak=∑k<nm+1ak=snm+1\sum_{j<m+1} B_j = s_{n_m} + B_m = \sum_{k<n_m} a_k + \sum_{k=n_m}^{n_{m+1}-1} a_k = \sum_{k<n_{m+1}} a_k = s_{n_{m+1}}, the middle equality being splitting at nm≤nm+1n_m \le n_{m+1}.

givenstep 1.1L1L2L5
3.1

By step 2.1 the partial sums of ∑Bj\sum B_j are precisely the terms snms_{n_m}, so ∑Bj\sum B_j converges with sum SS.

step 2.1step 1.2L3∎

Remarks

  • Why n0=0n_0 = 0 is a hypothesis and not a normalisation. If n0>0n_0 > 0 the same computation gives ∑j<mBj=snm−sn0\sum_{j<m} B_j = s_{n_m} - s_{n_0}, so the grouped series converges to S−sn0S - s_{n_0}: the terms a0,…,an0−1a_0, \dots, a_{n_0 - 1} are simply omitted. The theorem as stated is the case where nothing is omitted.

  • Blocks may be as long as one likes, and the theorem is indifferent. No bound on nj+1−njn_{j+1} - n_j is assumed, and none is needed: the argument never looks inside a block. This is exactly what fails in the converse direction, where the cancellation hidden inside long blocks is what the grouped series cannot see.

  • The result also gives the associativity one expects of a convergent series. Any two groupings of a convergent series have the same sum, both being SS; so one may insert brackets at will, though never remove them (FALSE: if some grouping of a series converges then the series itself converges).

Depends on

Used by

Dependency tree · next 3 levels

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