LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

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.

Convergence depends only on the tail

Statement

Let $(x_{k})$ be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences), let $x \in R$ , and for $K \in N$ let $x^{(K)}$ denote the $K$ -th tail, $x_{j}^{(K)} = x_{j + K}$ . The following are equivalent (Limits and Cauchy sequences of reals):

$(x_{k})$ converges to $x$ ;
every tail $x^{(K)}$ converges to $x$ ;
some tail $x^{(K)}$ converges to $x$ .

The same three statements with "converges to $x$ " replaced by "is Cauchy" are likewise equivalent. Consequently, if two sequences agree from some index on, then either both converge to $x$ or neither does, and either both are Cauchy or neither is.

Facts & Assumptions

Given: A sequence $(x_{k})$ of reals, a real $x$ , and for each $K \in N$ the $K$ -th tail $x^{(K)}$ defined by $x_{j}^{(K)} : = x_{j + K}$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L1]

Convergence and the Cauchy condition: $(z_{k})$ converges to $z$ when for every rational $ε > 0$ there is $N$ with $∣ z_{k} - z ∣ < ε$ for all $k \geq N$ , and $(z_{k})$ is Cauchy when for every rational $ε > 0$ there is $N$ with $∣ z_{k} - z_{l} ∣ < ε$ for all $k, l \geq N$ (Limits and Cauchy sequences of reals).

[L2]

Index arithmetic, first half: $j \geq N$ implies $j + K \geq N + K$ , and $N + K \geq N$ (Order on the natural numbers, Order is compatible with addition).

[L3]

Index arithmetic, second half: every $k \geq N + K$ has the form $k = j + K$ with $j \geq N$ . Indeed $N + K \leq k$ gives $i$ with $(N + K) + i = k$ ; put $j : = N + i$ , so that $j \geq N$ and $j + K = (N + i) + K = N + (i + K) = N + (K + i) = (N + K) + i = k$ (Order on the natural numbers, Addition is associative, Addition is commutative).

[L4]

The order on $N$ is reflexive and transitive, so $k \geq N + K \geq N$ gives $k \geq N$ ; and $j + 0 = j$ for every $j$ ( $\leq$ is a linear order on $N$ , Order on the natural numbers, Addition of natural numbers).

Proof

technique · direct

1.1

(1) implies (2). Assume $(x_{k})$ converges to $x$ , let $K \in N$ be arbitrary and let $ε > 0$ be rational; take $N$ with $∣ x_{k} - x ∣ < ε$ for all $k \geq N$ . For every $j \geq N$ we have $j + K \geq N + K \geq N$ , hence $∣ x_{j}^{(K)} - x ∣ = ∣ x_{j + K} - x ∣ < ε$ ; so $x^{(K)}$ converges to $x$ .

assume-hypL1L2L4

1.2

(2) implies (3), in both families. The $0$ -th tail satisfies $x_{j}^{(0)} = x_{j + 0} = x_{j}$ , so $(x_{k})$ is itself one of its own tails; statement (2) quantifies over all tails, so applying it to this one already yields (3).

givenL4

1.3

(3) implies (1). Assume $x^{(K)}$ converges to $x$ for some fixed $K$ , and let $ε > 0$ be rational; take $N$ with $∣ x_{j}^{(K)} - x ∣ < ε$ for all $j \geq N$ . Every $k \geq N + K$ is of the form $j + K$ with $j \geq N$ , so $∣ x_{k} - x ∣ = ∣ x_{j}^{(K)} - x ∣ < ε$ ; taking $N + K$ as the threshold shows $(x_{k})$ converges to $x$ .

assume-hypL1L3

1.4

The Cauchy version of (1) implies (2). Assume $(x_{k})$ is Cauchy, fix $K$ and a rational $ε > 0$ , and take $N$ with $∣ x_{k} - x_{l} ∣ < ε$ for all $k, l \geq N$ . For $i, j \geq N$ both $i + K \geq N$ and $j + K \geq N$ , so $∣ x_{i}^{(K)} - x_{j}^{(K)} ∣ = ∣ x_{i + K} - x_{j + K} ∣ < ε$ ; so $x^{(K)}$ is Cauchy.

assume-hypL1L2L4

1.5

The Cauchy version of (3) implies (1). Assume $x^{(K)}$ is Cauchy and let $ε > 0$ be rational; take $N$ with $∣ x_{i}^{(K)} - x_{j}^{(K)} ∣ < ε$ for all $i, j \geq N$ . Any $k, l \geq N + K$ are of the form $i + K$ and $j + K$ with $i, j \geq N$ , so $∣ x_{k} - x_{l} ∣ < ε$ ; so $(x_{k})$ is Cauchy.

assume-hypL1L3

2.1

In each of the two families the cycle (1) implies (2) implies (3) implies (1) is closed, so within each family the three statements are equivalent.

step 1.1step 1.2step 1.3step 1.4step 1.5

3.1

If $(x_{k})$ and $(y_{k})$ agree from index $K$ on, then $x^{(K)} = y^{(K)}$ as functions, so by the established equivalence $(x_{k})$ converges to $x$ exactly when $y^{(K)}$ does, exactly when $(y_{k})$ does, and the same chain applies to the Cauchy condition.

step 2.1given∎

Remarks

This is the lemma that makes the word "eventually" usable. Once it is known that finitely many initial terms are irrelevant, a hypothesis of the form " $P (k)$ for all $k$ " can everywhere be weakened to " $P (k)$ eventually" (Sequences of reals: bounded, eventually, frequently, tails, subsequences) at the cost of passing to a tail.
It also settles the bookkeeping question of where the indexing starts. A text that writes $(x_{k})_{k \geq 1}$ is describing the first tail of a sequence in the sense used here, and the two have the same limits and the same Cauchy status.
Boundedness, by contrast, is not a tail property in the same trivial way: a tail of a bounded sequence is bounded, and a sequence with a bounded tail is bounded only because the finitely many omitted terms can be absorbed into the bound, which is exactly the argument of Every convergent sequence is bounded.

Depends on

Used by

Dependency tree · two levels

22 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

J. K. Hunter, An Introduction to Real Analysis, Ch. 3 (standard reference, not scraped)
Limit of a sequence (Wikipedia) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §6.1 (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (standard reference, not scraped)