TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26

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.

Every contractive sequence is Cauchy, hence converges, with error bound $∣ x - x_{k} ∣ \leq c^{k - 1} ∣ x_{2} - x_{1} ∣ / (1 - c)$ for $k \geq 1$

Statement

Let $(x_{k})$ be a contractive sequence of reals with contraction constant $c$ , so $0 < c < 1$ and $∣ x_{k + 2} - x_{k + 1} ∣ \leq c ∣ x_{k + 1} - x_{k} ∣$ for every $k \in N$ (Contractive sequence: $∣ x_{k + 2} - x_{k + 1} ∣ \leq c ∣ x_{k + 1} - x_{k} ∣$ for a fixed $0 < c < 1$ ). Then:

Geometric decay of the gaps. For every $k \geq 1$ , $∣ x_{k + 1} - x_{k} ∣ \leq c^{k - 1} ∣ x_{2} - x_{1} ∣ .$
Convergence. $(x_{k})$ is Cauchy (Limits and Cauchy sequences of reals) and therefore converges to some $x \in R$ (The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges).
Error bound. For every $k \geq 1$ , $∣ x - x_{k} ∣ \leq \frac{c^{k - 1} ∣ x_{2} - x_{1} ∣}{1 - c} .$

The restriction $k \geq 1$ in claim 3 is a hypothesis, not a convention. The displayed bound is false at $k = 0$ , even though $c^{- 1}$ is defined (Integer powers $a^{m}$ ). Take $c = 1 / 2$ and the sequence $x_{0} = 0$ , $x_{k} = 1$ for all $k \geq 1$ : it is contractive with that $c$ , its limit is $x = 1$ , the right-hand side at $k = 0$ is $c^{- 1} ∣ x_{2} - x_{1} ∣ / (1 - c) = 2 \cdot 0 / (1 / 2) = 0$ , and the left-hand side is $∣ x - x_{0} ∣ = 1$ . The classical statement of this theorem is written for sequences indexed from $1$ , where the question does not arise; this library indexes from $0$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences), so the hypothesis is stated.

Facts & Assumptions

Given: A sequence $(x_{k})$ of reals and a real $c$ with $0 < c < 1$ such that $∣ x_{k + 2} - x_{k + 1} ∣ \leq c ∣ x_{k + 1} - x_{k} ∣$ for every $k \in N$ ; the abbreviations $D : = ∣ x_{2} - x_{1} ∣ \geq 0$ and $A : = D / (1 - c)$ , which is defined and $\geq 0$ since $1 - c > 0$ .

[L1]

Contractivity, with a constant independent of the index (Contractive sequence: $∣ x_{k + 2} - x_{k + 1} ∣ \leq c ∣ x_{k + 1} - x_{k} ∣$ for a fixed $0 < c < 1$ ).

[L2]

Induction principle (The principle of mathematical induction).

[L3]

Integer powers: $a^{0} = 1$ , $a^{k + 1} = a^{k} a$ ; and the law $a^{m + n} = a^{m} a^{n}$ (Integer powers $a^{m}$ , Laws of integer exponents).

[L4]

Powers and order: $a \geq 0$ gives $a^{n} \geq 0$ ; $1^{n} = 1$ for every $n$ (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ).

[L5]

Absolute value: $∣ t ∣ \geq 0$ , $∣ t ∣ = ∣ - t ∣$ , and $∣ t ∣ \leq u$ exactly when $- u \leq t \leq u$ (Basic properties of the absolute value).

[L6]

Multiplying inequalities of nonnegatives: $0 \leq a \leq b$ and $0 \leq e \leq f$ give $a e \leq b f$ (Multiplying inequalities of positives).

[L7]

Reciprocals of positives are positive (Inverses of positives are positive, and reciprocation reverses order).

[L8]

Finite sums, their notation $\sum_{i < n}$ , and their laws: additivity, scaling, monotonicity, and telescoping $\sum_{i < n} (t_{i + 1} - t_{i}) = t_{n} - t_{0}$ for any sequence $(t_{i})$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L9]

Triangle inequality for finite sums: $∣ \sum_{i < n} a_{i} ∣ \leq \sum_{i < n} ∣ a_{i} ∣$ (Triangle inequality for finite sums).

[L10]

Factorisation: $1 - c^{n} = (1 - c) \sum_{i < n} c^{i}$ , the case $b = 1$ , $a = c$ of $b^{n} - a^{n} = (b - a) \sum_{i = 0}^{n - 1} a^{i} b^{n - 1 - i}$ together with $1^{m} = 1$ ; at $n = 0$ both sides are $0$ (Factorisation of $b^{n} - a^{n}$ , and the resulting Lipschitz estimate, Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ).

[L11]

For $0 < c < 1$ the sequence $(c^{j})$ converges to $0$ (For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ ).

[L12]

Cauchy condition and convergence; it suffices to test a real $ε > 0$ , since every positive rational is a positive real (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L13]

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

[L14]

Limits: a sequence and each of its tails converge to the same limit (Convergence depends only on the tail); the algebra of limits (Algebra of limits: sums, scalar multiples, products and quotients); compatibility of the absolute value with limits (The absolute value is compatible with limits); and preservation of non-strict inequalities in the limit (Limits preserve non-strict inequalities).

[L15]

The order on $N$ is total, so any two indices are comparable ( $\leq$ is a linear order on $N$ ).

Proof

technique · induction

1.1

Base case of claim 1, at $k = 1$ : $∣ x_{2} - x_{1} ∣ \leq c^{0} ∣ x_{2} - x_{1} ∣ = D$ , since $c^{0} = 1$ .

givenL3base

1.2

Inductive hypothesis: fix $j \in N$ and assume $∣ x_{j + 2} - x_{j + 1} ∣ \leq c^{j} D$ .

1.3

By [L10], $(1 - c) \sum_{i < n} c^{i} = 1 - c^{n} \leq 1$ , since $c^{n} \geq 0$ ; dividing by $1 - c > 0$ gives $\sum_{i < n} c^{i} \leq 1 / (1 - c)$ .

givenL4L6L7L10

1.4

Let $ε > 0$ be an arbitrary real and put $δ : = ε / (2 (A + 1)) > 0$ , which is defined since $A + 1 > 0$ . By [L11] fix $J \in N$ with $c^{j} < δ$ for every $j \geq J$ .

givenL4L7L11L12choose

2.1

Successor step: contractivity at the index $j + 1$ gives $∣ x_{j + 3} - x_{j + 2} ∣ \leq c ∣ x_{j + 2} - x_{j + 1} ∣ \leq c \cdot c^{j} D = c^{j + 1} D$ , the middle inequality by the inductive hypothesis multiplied by $c > 0$ .

step 1.2L1L3L6

3.1

By the induction principle, $∣ x_{j + 2} - x_{j + 1} ∣ \leq c^{j} D$ for every $j \in N$ ; writing $k = j + 1$ this is claim 1: $∣ x_{k + 1} - x_{k} ∣ \leq c^{k - 1} D$ for every $k \geq 1$ .

step 1.1step 2.1L2

4.1

Fix $k \geq 1$ and $n \in N$ , and put $t_{i} : = x_{k + i}$ . Telescoping gives $x_{k + n} - x_{k} = t_{n} - t_{0} = \sum_{i < n} (t_{i + 1} - t_{i})$ , so $∣ x_{k + n} - x_{k} ∣ \leq \sum_{i < n} ∣ x_{k + i + 1} - x_{k + i} ∣$ .

step 3.1L8L9

4.2

Each summand obeys claim 1 at the index $k + i \geq 1$ : $∣ x_{k + i + 1} - x_{k + i} ∣ \leq c^{k + i - 1} D = c^{k - 1} c^{i} D$ .

step 3.1L3

5.1

Summing the bound of step 4.2 over $i < n$ , by monotonicity and scaling of finite sums, $∣ x_{k + n} - x_{k} ∣ \leq c^{k - 1} D \sum_{i < n} c^{i}$ .

step 4.1step 4.2L8

6.1

Combining steps 5.1 and 1.3: for every $k \geq 1$ and every $n \in N$ , $∣ x_{k + n} - x_{k} ∣ \leq c^{k - 1} D / (1 - c) = c^{k - 1} A$ .

step 5.1step 1.3L4L6

7.1

For all indices $l, k \geq J + 1$ : by comparability one of them is the smaller, say $k$ , and writing $l = k + n$ step 6.1 gives $∣ x_{l} - x_{k} ∣ \leq c^{k - 1} A \leq c^{k - 1} (A + 1) \leq δ (A + 1) = ε / 2 < ε$ , using $k - 1 \geq J$ ; the case $l < k$ follows since $∣ x_{l} - x_{k} ∣ = ∣ x_{k} - x_{l} ∣$ .

step 6.1step 1.4L5L6L15

8.1

The real $ε > 0$ was arbitrary and the index $J + 1$ was produced from it, so $(x_{k})$ is Cauchy, and therefore converges to some $x \in R$ : this is claim 2.

step 7.1L12L13

9.1

Fix $k \geq 1$ . The $k$ -th tail $n \mapsto x_{k + n}$ converges to $x$ , so as $n$ ranges over $N$ the sequence $n \mapsto x_{k + n} - x_{k}$ converges to $x - x_{k}$ , so $n \mapsto ∣ x_{k + n} - x_{k} ∣$ converges to $∣ x - x_{k} ∣$ ; the constant sequence with value $c^{k - 1} A$ converges to $c^{k - 1} A$ , and step 6.1 compares the two at every $n$ .

step 6.1step 8.1L14

10.1

Preservation of non-strict inequalities in the limit therefore gives $∣ x - x_{k} ∣ \leq c^{k - 1} A = c^{k - 1} ∣ x_{2} - x_{1} ∣ / (1 - c)$ for every $k \geq 1$ , which is claim 3; claims 1, 2 and 3 are thus all established.

step 3.1step 8.1step 9.1L14discharge-induction∎

Remarks

The bound is computable before the limit is known. Claim 3 needs only $c$ and the single number $∣ x_{2} - x_{1} ∣$ , so it is an a priori estimate of the error of the $k$ -th term: this is what makes contractive iteration a numerical method and not merely an existence theorem. The sequence $x_{k + 1} = (x_{k} + 1) / 3$ is contractive with $c = 1 / 3$ and converges to $1 / 2$ ↗ carries out the arithmetic on a concrete iteration.
Where completeness is spent. Only in step 10.1, through The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges. Claims 1 and 3 are inequalities that hold in any ordered field once the limit exists; it is the existence of the limit that needs the least-upper-bound property, and the theorem is exactly the shape in which the Cauchy criterion is usually applied, namely to prove convergence without exhibiting the limit.
A smaller constant is a better theorem. Any $c^{'} \in [c, 1)$ is also a contraction constant (Contractive sequence: $∣ x_{k + 2} - x_{k + 1} ∣ \leq c ∣ x_{k + 1} - x_{k} ∣$ for a fixed $0 < c < 1$ ), and the bound degrades as $c^{'}$ grows, tending to uselessness as $c^{'} \to 1$ . That degeneration is not an artefact: for gaps that merely shrink, with no uniform $c < 1$ , the conclusion fails outright ( $x_{k + 1} = x_{k} + 1 / x_{k}$ from $x_{1} = 1$ has strictly decreasing consecutive gaps and diverges, so no uniform $c < 1$ exists ↗).
On the index range. Claims 1 and 3 both start at $k = 1$ , and both are genuinely false at $k = 0$ , on the single witness given in the statement: there $∣ x_{1} - x_{0} ∣ = 1$ while $c^{- 1} ∣ x_{2} - x_{1} ∣ = 0$ , so claim 1 fails at $k = 0$ for the same reason claim 3 does. Nothing at all is asserted about the step from $x_{0}$ to $x_{1}$ , and nothing can be: the contractive hypothesis constrains every gap by its predecessor, and the first gap has no predecessor to be constrained by.

Depends on

Used by

Dependency tree · two levels

72 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

Cauchy sequence (Wikipedia) (standard reference, not scraped)
Contraction mapping (Wikipedia) (standard reference, not scraped)
R. Bartle and D. Sherbert, Introduction to Real Analysis, 4th ed., §3.5 (Thm 3.5.8) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §2.4 (standard reference, not scraped)
Contractive sequence (PlanetMath) (standard reference, not scraped)

Every contractive sequence is Cauchy, hence converges, with error bound ∣x−xk∣≤ck−1∣x2−x1∣/(1−c)∣x−xk​∣≤ck−1∣x2​−x1​∣/(1−c) for k≥1k≥1