ExampleConstruction: Literature-sourcedVerification: 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.

The Babylonian sequence $x_{1} = 2$ , $x_{k + 1} = (x_{k} + 2 / x_{k}) / 2$ decreases to $\sqrt{2}$

Example

Let $(x_{k})_{k \geq 1}$ be given by

$x_{1} = 2, x_{k + 1} = \frac{1}{2} (x_{k} + \frac{2}{x_{k}}) (k \geq 1) .$

Then $(x_{k})$ is strictly decreasing, every term satisfies $x_{k} > \sqrt{2}$ , and

$\lim_{k} x_{k} = \sqrt{2} .$

This is the Babylonian, or Heron, iteration for the square root, and it is the standard illustration of A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum: monotone plus bounded delivers a limit, and the recursion then identifies the limit, because the limit must be a fixed point of the map that produced the sequence.

Indexing. Sequences in this library are functions on $N$ , which starts at $0$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences). The family above, indexed from $1$ , is realised as $x_{k} : = g_{k - 1}$ for the sequence $(g_{j})_{j \in N}$ with $g_{0} = 2$ and $g_{j + 1} = (g_{j} + 2 / g_{j}) / 2$ , and the verification below works with $(g_{j})$ . The shift changes nothing: convergence and monotonicity read the same under it (Convergence depends only on the tail).

Facts & Assumptions

Given: The set $A : = {u \in R : u > 0}$ , the element $2 \in A$ , and the function $f : A \to A$ with $f (u) = (u + 2 / u) / 2$ , which does land in $A$ because $u > 0$ gives $2 / u > 0$ and hence $f (u) > 0$ ; by the recursion theorem (The recursion theorem) the unique $g : N \to A$ with $g_{0} = 2$ and $g_{j + 1} = f (g_{j})$ . We write $x_{k} : = g_{k - 1}$ for $k \geq 1$ , so $x_{1} = 2$ and $x_{k + 1} = f (x_{k})$ .

[L1]

Recursion theorem (The recursion theorem) and the induction principle (The principle of mathematical induction).

[L2]

Square roots: every $a \geq 0$ has a unique $s \geq 0$ with $s^{2} = a$ ; in particular $(\sqrt{2})^{2} = 2$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Integer powers $a^{m}$ ).

[L3]

Powers and order: for $a, b \geq 0$ , $a < b$ exactly when $a^{2} < b^{2}$ (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ).

[L4]

A nonzero square is positive: $t \neq 0$ gives $t^{2} > 0$ (Squares of nonzero elements are positive).

[L5]

Order and arithmetic: $1 > 0$ , hence $2 = 1 + 1 > 0$ and $2 > 1$ ; sums of positives are positive; adding a constant preserves the order; a positive has a positive inverse, and a quotient of positives is positive (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, Ordered field, Complete ordered field (least-upper-bound property)).

[L6]

Monotone sequences, with consecutive comparisons sufficing (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences), and boundedness below of a subset of $R$ (Lower bound, bounded below, bounded set).

[L7]

Monotone convergence: a nonincreasing sequence whose range is bounded below converges, to the infimum of its range (A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum, Limits and Cauchy sequences of reals).

[L8]

Algebra of limits, including the quotient case when the denominators and the limit are nonzero (Algebra of limits: sums, scalar multiples, products and quotients); limits preserve non-strict inequalities (Limits preserve non-strict inequalities); 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.1givenL5

Every term is positive, since $g$ takes values in $A$ by construction.

1.2givenL1L4L5

By induction, $(g_{j})^{2} > 2$ for every $j$ . Base: $(g_{0})^{2} = 4 > 2$ . Step: assuming $(g_{j})^{2} > 2$ , the identity $(g_{j + 1})^{2} - 2 = (\frac{(g_{j})^{2} - 2}{2 g_{j}})^{2}$ holds by field arithmetic, and its right-hand side is the square of a nonzero element, since $(g_{j})^{2} - 2 > 0$ and $2 g_{j} > 0$ , hence is $> 0$ .

2.1step 1.1step 1.2L2L3

Every term satisfies $g_{j} > \sqrt{2}$ : both $g_{j}$ and $\sqrt{2}$ are $\geq 0$ , and $(\sqrt{2})^{2} = 2 < (g_{j})^{2}$ .

2.2step 1.1step 1.2L5L6

The sequence is strictly decreasing: $g_{j} - g_{j + 1} = g_{j} - \frac{1}{2} (g_{j} + 2 / g_{j}) = \frac{(g_{j})^{2} - 2}{2 g_{j}} > 0$ , since the numerator is positive by step 1.2 and the denominator by step 1.1; consecutive comparisons then give strict decrease, hence also that $(g_{j})$ is nonincreasing.

3.1step 2.1step 2.2L6L7

The range of $(g_{j})$ is bounded below by $\sqrt{2}$ , so by monotone convergence $(g_{j})$ converges; write $L$ for its limit.

4.1step 2.1step 3.1L2L4L8

$L \geq \sqrt{2}$ : the inequality $g_{j} > \sqrt{2}$ holds at every index, so it passes to the limit in its non-strict form. In particular $L > 0$ , since $\sqrt{2} > 0$ by $(\sqrt{2})^{2} = 2 > 0$ and $\sqrt{2} \geq 0$ .

5.1step 1.1step 3.1step 4.1L8

By the algebra of limits, using $g_{j} \neq 0$ for every $j$ and $L \neq 0$ , the sequence $j \mapsto \frac{1}{2} (g_{j} + 2 / g_{j})$ converges to $\frac{1}{2} (L + 2 / L)$ .

6.1step 3.1L8

The sequence $j \mapsto g_{j + 1}$ is the first tail of $(g_{j})$ , so it also converges to $L$ ; and it is the same sequence as in step 5.1, by the recursion clause.

7.1step 5.1step 6.1L8L5

By uniqueness of limits, $L = \frac{1}{2} (L + 2 / L)$ , hence $2 L = L + 2 / L$ , hence $L = 2 / L$ and $L^{2} = 2$ .

8.1step 4.1step 7.1step 2.1step 2.2L2∎

Since $L \geq 0$ and $L^{2} = 2$ , uniqueness of the nonnegative square root gives $L = \sqrt{2}$ . So $(g_{j})$ , and with it $(x_{k})$ , is strictly decreasing, stays above $\sqrt{2}$ , and converges to $\sqrt{2}$ .

Remarks

The identification of the limit is the interesting half. Monotone convergence produces $L$ but says only that it is the infimum of the range, which is not a usable description. Passing to the limit in the recursion turns the description into an equation, $L = (L + 2 / L) / 2$ , and that equation has exactly one nonnegative solution. The step that makes this legitimate is Convergence depends only on the tail: the shifted sequence $(g_{j + 1})$ has the same limit as $(g_{j})$ , so the two sides of the recursion may be compared in the limit.
The hypothesis $L \neq 0$ is not free. The quotient case of Algebra of limits: sums, scalar multiples, products and quotients requires it, and it is supplied by step 4.1, not assumed. Had the sequence been allowed to approach $0$ the argument would break exactly there, and this is the usual place where a proof of this example is incomplete.
Convergence is very fast, though nothing above uses that. The identity in step 1.2 also gives $g_{j + 1} - \sqrt{2} = (g_{j} - \sqrt{2})^{2} / (2 g_{j})$ , so the error is squared at each step: the iteration is Newton's method applied to $u^{2} - 2$ . The contractive estimate 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$ would give only geometric decay, so it is a weaker tool here, and the monotone route is both shorter and sharper.
Nothing in the argument is special to $2$ . The same proof with $2$ replaced by any $a > 0$ , starting from any $x_{1} > 0$ with $x_{1}^{2} > a$ , converges to $\sqrt{a}$ . The starting value $2$ is chosen because $2^{2} = 4 > 2$ makes the base case of step 1.2 immediate.

The Babylonian sequence $x_{1} = 2$ , $x_{k + 1} = (x_{k} + 2 / x_{k}) / 2$ decreases to $\sqrt{2}$

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources

The Babylonian sequence x1=2x1​=2, xk+1=(xk+2/xk)/2xk+1​=(xk​+2/xk​)/2 decreases to 22​

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources

The Babylonian sequence $x_{1} = 2$ , $x_{k + 1} = (x_{k} + 2 / x_{k}) / 2$ decreases to $\sqrt{2}$