ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passverified 2026-08-06 (claude-sonnet-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.

The sequence $x_{k + 1} = (x_{k} + 1) / 3$ is contractive with $c = 1 / 3$ and converges to $1 / 2$

Example

Fix any $a \in R$ and let $(x_{k})$ be the sequence with $x_{0} = a$ and

$x_{k + 1} = \frac{x_{k} + 1}{3} (k \in N) .$

Then $(x_{k})$ is contractive with contraction constant $c = 1 / 3$ (Contractive sequence: $∣ x_{k + 2} - x_{k + 1} ∣ \leq c ∣ x_{k + 1} - x_{k} ∣$ for a fixed $0 < c < 1$ ), and

$\lim_{k} x_{k} = \frac{1}{2},$

whatever the starting value $a$ is. Moreover 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$ supplies the error bound $∣ 1 / 2 - x_{k} ∣ \leq 3^{- (k - 1)} ∣ x_{2} - x_{1} ∣ / (1 - 1 / 3)$ for $k \geq 1$ , which is computable from the first three terms alone.

The limit $1 / 2$ is the unique solution of $L = (L + 1) / 3$ , that is the unique fixed point of the map $u \mapsto (u + 1) / 3$ . This is the smallest honest instance of the Banach fixed point theorem: a contraction on $R$ has one fixed point, and every orbit converges to it.

Facts & Assumptions

Given: A real $a$ , and by the recursion theorem (The recursion theorem) applied to $R$ , the element $a$ and the function $f (u) = (u + 1) / 3$ , the unique sequence $(x_{k})$ of reals with $x_{0} = a$ and $x_{k + 1} = f (x_{k})$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences); the constant $c : = 1 / 3$ .

[L1]

Recursion theorem (The recursion theorem).

[L2]

Order and arithmetic: $1 > 0$ , so $3 = 1 + 1 + 1 > 1 > 0$ ; a positive has a positive inverse; and $0 < r < 1$ exactly when $1 / r > 1$ , so $0 < 1 / 3 < 1$ (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Inverses of positives are positive, and reciprocation reverses order, Reciprocals and order: $1 / r$ against $1$ , Ordered field, Complete ordered field (least-upper-bound property)).

[L3]

Field arithmetic: $(u + 1) / 3 - (v + 1) / 3 = (u - v) / 3$ , and $3 L = L + 1$ is equivalent to $2 L = 1$ (Field).

[L4]

Absolute value: $∣ a b ∣ = ∣ a ∣ ∣ b ∣$ , and $∣ t ∣ = t$ for $t \geq 0$ , so $∣ (u - v) / 3 ∣ = ∣ u - v ∣ / 3$ (Basic properties of the absolute value).

[L5]

Contractive sequences: a constant $c$ with $0 < c < 1$ and $∣ x_{k + 2} - x_{k + 1} ∣ \leq c ∣ x_{k + 1} - x_{k} ∣$ at every index (Contractive sequence: $∣ x_{k + 2} - x_{k + 1} ∣ \leq c ∣ x_{k + 1} - x_{k} ∣$ for a fixed $0 < c < 1$ ).

[L6]

Every contractive sequence is Cauchy and converges, with the stated error bound for $k \geq 1$ (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$ , Limits and Cauchy sequences of reals).

[L7]

Algebra of limits (Algebra of limits: sums, scalar multiples, products and quotients); a sequence and its tails have the same limits (Convergence depends only on the tail); limits are unique (A sequence has at most one limit).

Verification

technique · direct

1.1

The constant $c = 1 / 3$ satisfies $0 < c < 1$ .

givenL2

1.2

For every $k$ : $x_{k + 2} - x_{k + 1} = \frac{x_{k + 1} + 1}{3} - \frac{x_{k} + 1}{3} = \frac{x_{k + 1} - x_{k}}{3}$ , so $∣ x_{k + 2} - x_{k + 1} ∣ = \frac{1}{3} ∣ x_{k + 1} - x_{k} ∣$ .

givenL1L3L4

2.1

Hence $(x_{k})$ is contractive with contraction constant $c = 1 / 3$ , the inequality of [L5] holding with equality at every index.

step 1.1step 1.2L5

3.1

By [L6] the sequence converges; write $L$ for its limit, and the error bound of [L6] holds for it with $c = 1 / 3$ .

step 2.1L6

4.1

The sequence $k \mapsto x_{k + 1}$ is the first tail of $(x_{k})$ , so it converges to $L$ ; and by the algebra of limits $k \mapsto (x_{k} + 1) / 3$ converges to $(L + 1) / 3$ .

step 3.1L7

5.1

The two sequences of step 4.1 are the same sequence, by the recursion clause, so uniqueness of limits gives $L = (L + 1) / 3$ , hence $3 L = L + 1$ , hence $2 L = 1$ and $L = 1 / 2$ .

step 4.1L1L3L7

6.1

So for every starting value $a$ the sequence is contractive with $c = 1 / 3$ and converges to $1 / 2$ , with the error bound of step 3.1.

step 2.1step 3.1step 5.1∎

Remarks

The starting value is genuinely arbitrary. Nothing in the verification uses anything about $a$ , and the limit does not depend on it. What does depend on it is the error bound, through $∣ x_{2} - x_{1} ∣$ , which for this recursion equals $∣ a - 1 / 2 ∣ \cdot 2 / 9$ .
Contractivity is exact here, not an estimate. Step 1.2 gives equality, $∣ x_{k + 2} - x_{k + 1} ∣ = \frac{1}{3} ∣ x_{k + 1} - x_{k} ∣$ , so for every starting value $a \neq 1 / 2$ the constant $c = 1 / 3$ is the smallest admissible one; for $a = 1 / 2$ the sequence is constant, every gap is $0$ , and every $c \in (0, 1)$ is admissible (Contractive sequence: $∣ x_{k + 2} - x_{k + 1} ∣ \leq c ∣ x_{k + 1} - x_{k} ∣$ for a fixed $0 < c < 1$ ). The error bound of 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$ is as sharp as that theorem can make it. Contrast $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, where the ratio of consecutive gaps tends to $1$ and no admissible constant exists at all.
Why a fixed point is forced. The limit satisfies the recursion equation because a sequence and its shift have the same limit (Convergence depends only on the tail) and the algebra of limits transports the right-hand side. This is the same move as in The Babylonian sequence $x_{1} = 2$ , $x_{k + 1} = (x_{k} + 2 / x_{k}) / 2$ decreases to $\sqrt{2}$ and The sequence $x_{1} = 1$ , $x_{k + 1} = \sqrt{2 + x_{k}}$ increases to $2$ ; the difference is that here convergence comes from contractivity rather than from monotonicity, and no monotonicity is available, since for $a > 1 / 2$ the sequence decreases and for $a < 1 / 2$ it increases while for $a = 1 / 2$ it is constant.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

50 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

Fixed-point iteration (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 (standard reference, not scraped)

The sequence xk+1=(xk+1)/3xk+1​=(xk​+1)/3 is contractive with c=1/3c=1/3 and converges to 1/21/2