ExampleConstruction: AI-adaptedVerification: 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 sequence $x_{1} = 1$ , $x_{k + 1} = \sqrt{2 + x_{k}}$ increases to $2$

Example

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

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

Then $(x_{k})$ is strictly increasing, every term satisfies $0 \leq x_{k} < 2$ , and

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

Informally this is the value of the nested radical $\sqrt{2 + \sqrt{2 + \sqrt{2 + \dots}}}$ , and the point of the example is that the expression means nothing until the sequence is shown to converge; only then does passing to the limit in the recursion identify the value.

Indexing. As in The Babylonian sequence $x_{1} = 2$ , $x_{k + 1} = (x_{k} + 2 / x_{k}) / 2$ decreases to $\sqrt{2}$ , the family indexed from $1$ is realised as $x_{k} : = g_{k - 1}$ for the sequence $(g_{j})_{j \in N}$ with $g_{0} = 1$ and $g_{j + 1} = \sqrt{2 + g_{j}}$ , and the verification works with $(g_{j})$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Convergence depends only on the tail).

Facts & Assumptions

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

[L1]

Recursion theorem (The recursion theorem).

[L2]

Square roots: every $a \geq 0$ has a unique $s \geq 0$ with $s^{2} = a$ (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}$ , and $a \leq b$ exactly when $a^{2} \leq b^{2}$ (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ).

[L4]

Order and arithmetic: $1 > 0$ , so $2 = 1 + 1 > 0$ and $4 = 2 \cdot 2$ ; adding a constant preserves the order, and inequalities may be added (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Ordered field, Complete ordered field (least-upper-bound property)).

[L5]

A field has no zero divisors: $u v = 0$ forces $u = 0$ or $v = 0$ (A field has no zero divisors: $a b = 0 \Rightarrow a = 0$ or $b = 0$ ).

[L6]

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

[L7]

Monotone convergence: a nondecreasing sequence whose range is bounded above converges, to the supremum 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 (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.1

The function $f$ does map $A$ into $A$ , so the construction is legitimate: for $0 \leq u < 2$ we have $2 \leq 2 + u < 4$ , hence $\sqrt{2 + u} \geq 0$ and $(\sqrt{2 + u})^{2} = 2 + u < 4 = 2^{2}$ , which gives $\sqrt{2 + u} < 2$ .

givenL2L3L4

1.2

Consequently every term satisfies $0 \leq g_{j} < 2$ , since $g$ takes its values in $A$ .

givenL1

2.1

The sequence is strictly increasing. Fix $j$ . From $0 \leq g_{j} < 2$ we get $g_{j} - 2 < 0$ and $g_{j} + 1 > 0$ , so $(g_{j} - 2) (g_{j} + 1) < 0$ , that is $(g_{j})^{2} - g_{j} - 2 < 0$ , that is $(g_{j})^{2} < 2 + g_{j} = (g_{j + 1})^{2}$ . Since $g_{j} \geq 0$ and $g_{j + 1} \geq 0$ , this gives $g_{j} < g_{j + 1}$ ; consecutive comparisons then give strict increase, hence also that $(g_{j})$ is nondecreasing.

step 1.2L2L3L4L6

3.1

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

step 1.2step 2.1L6L7

4.1

$1 \leq L \leq 2$ : the inequalities $1 = g_{0} \leq g_{j} \leq 2$ hold at every index, by step 2.1 and step 1.2, and pass to the limit in their non-strict form.

step 1.2step 2.1step 3.1L8

4.2

The sequence $j \mapsto g_{j + 1}$ is the first tail of $(g_{j})$ , so it converges to $L$ , and therefore $j \mapsto (g_{j + 1})^{2}$ converges to $L^{2}$ by the algebra of limits.

step 3.1L8

4.3

The same sequence satisfies $(g_{j + 1})^{2} = 2 + g_{j}$ for every $j$ , and $j \mapsto 2 + g_{j}$ converges to $2 + L$ .

step 3.1L8L2

5.1

By uniqueness of limits, $L^{2} = 2 + L$ , that is $(L - 2) (L + 1) = 0$ .

step 4.2step 4.3L8

6.1

Since $L \geq 1$ we have $L + 1 \geq 2 > 0$ , so $L + 1 \neq 0$ , and a field has no zero divisors, so $L - 2 = 0$ and $L = 2$ . Thus $(g_{j})$ , and with it $(x_{k})$ , is strictly increasing, lies in $[0, 2)$ , and converges to $2$ .

step 4.1step 5.1step 1.2step 2.1L4L5∎

Remarks

The limit is not attained. Every term is strictly below $2$ and the limit is $2$ , which is the supremum of the range and does not belong to it. That is the ordinary situation for a strictly increasing convergent sequence, and it is why A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum is stated with a supremum rather than a maximum.
The quadratic has two roots and only one is admissible. The limit equation $L^{2} = 2 + L$ is solved by $L = 2$ and by $L = - 1$ . The second is excluded by step 4.1, which is why the bound $L \geq 1$ is proved rather than waved through: without it the argument would identify the limit only up to a sign, and a reader who writes down the limit equation without checking the range of $L$ has proved strictly less than the example claims.
Squaring the recursion avoids a continuity argument. Passing to the limit in $g_{j + 1} = \sqrt{2 + g_{j}}$ directly would need continuity of the square root, which this library has not proved at this point. Squaring first turns the recursion into $(g_{j + 1})^{2} = 2 + g_{j}$ , in which only the algebra of limits is required. The device is worth remembering: an identity between polynomials in the terms passes to the limit for free, whereas an identity involving a function does not.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

54 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

Nested radical (Wikipedia) (standard reference, not scraped)
Monotone convergence theorem (Wikipedia) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §6.3 (standard reference, not scraped)
J. Lebl, Basic Analysis I, §2.2 (standard reference, not scraped)

The sequence x1=1x1​=1, xk+1=2+xkxk+1​=2+xk​​ increases to 22