ExampleConstruction: AI-adaptedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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 successive differences $\sqrt{k + 1} - \sqrt{k}$ converge to $0$

Example

The sequence $z_{k} : = \sqrt{k + 1} - \sqrt{k}$ converges to $0$ (Limits and Cauchy sequences of reals). Since $(\sqrt{k + 1} - \sqrt{k}) (\sqrt{k + 1} + \sqrt{k}) = 1$ , the differences are the reciprocals of the sequence $w_{k} : = \sqrt{k + 1} + \sqrt{k}$ , which diverges to $+ \infty$ because $w_{k} \geq \sqrt{k}$ and $(\sqrt{k})$ does (The square roots $\sqrt{k}$ diverge to $+ \infty$ ); the backward direction of For positive terms, null and divergence to $+ \infty$ are reciprocal then gives $z_{k} \to 0$ . Thus a difference of two sequences that both diverge can converge, so the algebra of limits has no difference rule for divergent sequences.

Facts & Assumptions

Given: For every natural $k$ the reals $\sqrt{k}$ and $\sqrt{k + 1}$ , with $k + 1 = σ (k)$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences), and the sequences $z_{k} : = \sqrt{k + 1} - \sqrt{k}$ , $w_{k} : = \sqrt{k + 1} + \sqrt{k}$ .

[F1]

$(\sqrt{k})_{k \in N}$ diverges to $+ \infty$ (The square roots $\sqrt{k}$ diverge to $+ \infty$ ).

[F2]

Reciprocal bridge: for a sequence $(x_{k})$ with $x_{k} > 0$ for every $k$ , $(x_{k})$ converges to $0$ if and only if $(1 / x_{k})$ diverges to $+ \infty$ (For positive terms, null and divergence to $+ \infty$ are reciprocal).

[F3]

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

[F4]

Divergence to $+ \infty$ : $x_{k} \to + \infty$ means that for every real $M$ there is $K$ with $x_{k} > M$ for all $k \geq K$ (Divergence to $+ \infty$ and to $- \infty$ ).

[F5]

Field arithmetic: every nonzero element has a multiplicative inverse, and $u v = 1$ with $v$ the inverse of $u$ identifies $v = u^{- 1}$ (Field).

[F6]

Monotonicity of squaring on nonnegatives: for $a, b \geq 0$ , $a < b ⟺ a^{2} < b^{2}$ and $a \leq b ⟺ a^{2} \leq b^{2}$ (Squaring is monotone on the nonnegatives).

[F7]

Adding inequalities: if $a < b$ and $c < d$ then $a + c < b + d$ , and translation by a constant preserves the order (Order is preserved by adding a constant and by adding inequalities).

[F8]

$0 < 1$ (The multiplicative identity is positive).

[F9]

Archimedean property: for every real $x$ there is a natural number $n \geq 1$ with $x < n \cdot 1_{R}$ (Every complete ordered field is Archimedean).

[F10]

Canonical naturals: $k + 1 \geq 1$ for every $k$ , and $n \mapsto n \cdot 1_{R}$ is strictly increasing, hence preserves non-strict order, on ${1, 2, 3, \dots}$ (Canonical naturals are positive and strictly increasing).

[F11]

Inverses of positives are positive: $a > 0$ implies $a^{- 1} > 0$ (Inverses of positives are positive, and reciprocation reverses order).

Verification

technique · direct

1.1givenF3F5F6F7F8F10

For every $k$ , $(\sqrt{k + 1})^{2} = k + 1$ and $(\sqrt{k})^{2} = k$ by [F3], so the product of the two factors is $z_{k} w_{k} = (\sqrt{k + 1} - \sqrt{k}) (\sqrt{k + 1} + \sqrt{k}) = (k + 1) - k = 1$ by [F5] and algebra. Moreover $w_{k} > 0$ : both roots are nonnegative by [F3], $1 \leq k + 1$ by [F10] with $1^{2} = 1 \leq k + 1 = (\sqrt{k + 1})^{2}$ gives $1 \leq \sqrt{k + 1}$ by [F6], and adding the nonnegative $\sqrt{k}$ to it preserves the inequality by [F7], so $w_{k} \geq \sqrt{k + 1} \geq 1 > 0$ by [F8]. Since $w_{k} \neq 0$ , the identity $z_{k} w_{k} = 1$ exhibits $z_{k}$ as the inverse of $w_{k}$ by [F5].

1.2givenF3F7

For every $k$ , $0 \leq \sqrt{k + 1}$ by [F3]; adding $\sqrt{k}$ to this inequality gives $\sqrt{k} \leq \sqrt{k + 1} + \sqrt{k} = w_{k}$ . Translation preserves a non-strict inequality by [F7] in the strict case and by equality otherwise.

1.3givenF3F4F6F9F10

The shifted sequence $(\sqrt{k + 1})$ diverges to $+ \infty$ : given a real $M$ , if $M < 0$ then $\sqrt{k + 1} \geq 0 > M$ for every $k$ by [F3]; if $M \geq 0$ , [F9] gives a natural $n \geq 1$ with $M^{2} < n$ , and for every $k \geq n$ one has $n \leq k + 1$ by [F10], hence $M^{2} < (\sqrt{k + 1})^{2}$ ; since $M \geq 0$ and $\sqrt{k + 1} \geq 0$ , the equivalence of [F6] gives $M < \sqrt{k + 1}$ . So for every real $M$ the bound holds eventually, which is [F4].

2.1step 1.2F1F4

The sequence $(w_{k})$ diverges to $+ \infty$ : by [F1] the sequence $(\sqrt{k})$ does, so given a real $M$ there is $K$ with $\sqrt{k} > M$ for all $k \geq K$ , and step 1.2 gives $w_{k} \geq \sqrt{k} > M$ there; this is the condition of [F4].

3.1step 1.1step 1.3step 2.1F1F2F5F11∎

Put $x_{k} : = 1 / w_{k}$ . Since $w_{k} > 0$ for every $k$ by step 1.1, [F11] gives $x_{k} > 0$ for every $k$ , and $1 / x_{k} = 1 / (1 / w_{k}) = w_{k}$ by [F5]. Now $1 / x_{k} = w_{k}$ diverges to $+ \infty$ by step 2.1, so the backward direction of the reciprocal bridge [F2], applied to the positive sequence $(x_{k})$ , gives $x_{k} = 1 / w_{k} \to 0$ ; and $z_{k} = w_{k}^{- 1} = 1 / w_{k}$ by step 1.1, so $z_{k} \to 0$ . Moreover $(\sqrt{k})$ diverges to $+ \infty$ by [F1] and $(\sqrt{k + 1})$ does by step 1.3, so $z_{k}$ is the difference of two sequences that both diverge to $+ \infty$ and yet converges to $0$ : the algebra of limits has no difference rule for divergent sequences.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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

John K. Hunter, An Introduction to Real Analysis (complete author-hosted lecture notes, 307 pp.) (standard reference, not scraped)
Jiri Lebl, Basic Analysis I: Introduction to Real Analysis, Volume I (author-hosted complete book PDF) (standard reference, not scraped)

The successive differences k+1−kk+1​−k​ converge to 00