ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

$(-1)^k$ has $\liminf = -1$ and $\limsup = 1$ , so it does not converge

Example

Let $(s_k)$ be the alternating sequence of The even and odd index maps and the alternating sequence: strictly increasing $e, o$ with $\mathbb{N}$ their disjoint union, and the unique $(s_k)$ with $s_0 = 1$ , $s_{\sigma(k)} = -s_k$ , which satisfies $|s_k| = 1$ , $s \circ e \equiv 1$ and $s \circ o \equiv -1$ , the sequence usually written $s_k = (-1)^k$ , characterised by $s_0 = 1$ and $s_{k+1} = -s_k$ . Then

$\liminf_{k} s_k = -1, \qquad \limsup_{k} s_k = 1,$

so the two differ and $(s_k)$ neither converges nor diverges to $\pm\infty$ (A real sequence converges to $L \in \mathbb{R}$ iff $\liminf x_k = \limsup x_k = L$ , and diverges to $\pm\infty$ iff both equal $\pm\infty$ ).

This is the smallest example in which the inequality $\liminf \le \limsup$ is strict, and it shows exactly what the gap measures: the sequence keeps returning to two different values, and neither of them can be the limit because the other keeps interrupting.

Facts & Assumptions

Given: The alternating sequence $(s_k)$ and the index maps $e, o$ of The even and odd index maps and the alternating sequence: strictly increasing $e, o$ with $\mathbb{N}$ their disjoint union, and the unique $(s_k)$ with $s_0 = 1$ , $s_{\sigma(k)} = -s_k$ , which satisfies $|s_k| = 1$ , $s \circ e \equiv 1$ and $s \circ o \equiv -1$ , and the tail ranges $T_n = \{s_k : k \ge n\}$ with extended tail bounds $s\!\sup_n := \sup T_n$ and $s\!\inf_n := \inf T_n$ (Limit superior and limit inferior of a real sequence as $\inf_n \sup_{k \ge n} x_k$ and $\sup_n \inf_{k \ge n} x_k$ in $\overline{\mathbb{R}}$ ).

[L1]

The alternating sequence: $|s_k| = 1$ for every $k$ , $s_{e_j} = 1$ and $s_{o_j} = -1$ for every $j$ , and $e$ , $o$ are strictly increasing (The even and odd index maps and the alternating sequence: strictly increasing $e, o$ with $\mathbb{N}$ their disjoint union, and the unique $(s_k)$ with $s_0 = 1$ , $s_{\sigma(k)} = -s_k$ , which satisfies $|s_k| = 1$ , $s \circ e \equiv 1$ and $s \circ o \equiv -1$ ).

[L2]

A strictly increasing index map satisfies $n_j \ge j$ (A strictly increasing index map satisfies $n_k \ge k$ ).

[L3]

Limit superior and limit inferior: $\limsup_k z_k = \inf\{\sup T_n(z)\}$ and $\liminf_k z_k = \sup\{\inf T_n(z)\}$ , all four kinds of bound existing in $\overline{\mathbb{R}}$ for every sequence, the supremum being the least upper bound and the infimum the greatest lower bound (Limit superior and limit inferior of a real sequence as $\inf_n \sup_{k \ge n} x_k$ and $\sup_n \inf_{k \ge n} x_k$ in $\overline{\mathbb{R}}$ , The tail suprema of any real sequence are nonincreasing in $\overline{\mathbb{R}}$ , so the limit superior exists for every sequence, Every subset of $\overline{\mathbb{R}}$ has a least upper bound and a greatest lower bound in $\overline{\mathbb{R}}$ , agreeing with the real supremum and infimum on nonempty sets bounded in $\mathbb{R}$ , Upper bound, least upper bound, and strict upper bound, Partial order and partially ordered set, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L4]

The order on $\overline{\mathbb{R}}$ is total and restricts on $\mathbb{R}$ to the order of $\mathbb{R}$ (The extended real line $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$ , its order, and the arithmetic that is left undefined).

[L5]

Absolute value: $|t| = 1$ forces $t = 1$ or $t = -1$ (Basic properties of the absolute value, Absolute value in an ordered field).

[L6]

Order arithmetic: $0 < 1$ , hence $-1 < 1$ and $-1 \ne 1$ (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)).

[L7]

A real sequence converges to $L \in \mathbb{R}$ exactly when $\liminf = \limsup = L$ , and diverges to $\pm\infty$ exactly when both equal $\pm\infty$ (A real sequence converges to $L \in \mathbb{R}$ iff $\liminf x_k = \limsup x_k = L$ , and diverges to $\pm\infty$ iff both equal $\pm\infty$ ).

Verification

technique · direct

1.1

Every value of the sequence is $1$ or $-1$ , since $|s_k| = 1$ .

givenL1L5

1.2

For every $n \in \mathbb{N}$ both values occur at some index $\ge n$ : $s_{e_n} = 1$ with $e_n \ge n$ , and $s_{o_n} = -1$ with $o_n \ge n$ .

givenL1L2

2.1

Hence $T_n = \{1, -1\}$ for every $n$ . Its least upper bound in $\overline{\mathbb{R}}$ is $1$ , since $1$ bounds both elements from above, using $-1 < 1$ , and any upper bound is $\ge 1$ because $1 \in T_n$ ; dually its greatest lower bound is $-1$ .

step 1.1step 1.2L3L4L6

3.1

Therefore the family of tail suprema is the one-element family $\{1\}$ , whose greatest lower bound is $1$ , so $\limsup_k s_k = 1$ ; and the family of tail infima is $\{-1\}$ , whose least upper bound is $-1$ , so $\liminf_k s_k = -1$ .

step 2.1L3L4

4.1

Since $-1 \ne 1$ , there is no $L$ with $\liminf_k s_k = \limsup_k s_k = L$ , so by [L7] the sequence converges to no real number and diverges to neither $+\infty$ nor $-\infty$ .

step 3.1L6L7∎

Remarks

The two values are exactly the subsequential limits. By The limit superior is itself a subsequential limit in $\overline{\mathbb{R}}$ and is the greatest one and The limit inferior is the least subsequential limit in $\overline{\mathbb{R}}$ the numbers $1$ and $-1$ are the greatest and least elements of $\overline{\operatorname{SL}}(s)$ , and since every term is $1$ or $-1$ no other value can be a subsequential limit, so $\operatorname{SL}(s) = \{-1, 1\}$ exactly.
Contrast with The sequence $(-1)^k(1 + 1/k)$ is bounded with subsequential limit set exactly $\{-1, 1\}$ . There the same two subsequential limits arise for a sequence none of whose terms equals either of them. The limit superior and limit inferior do not care: they are determined by the tails, not by whether the values are attained.
This sequence is the standard witness for strictness throughout the page. It drives FALSE: $\limsup(x_k + y_k) = \limsup x_k + \limsup y_k$ and $x_k = (-1)^k$ , $y_k = (-1)^{k+1}$ give $\limsup(x_k + y_k) = 0 < 2 = \limsup x_k + \limsup y_k$ , and, after an affine change, $x_k = 1 + (-1)^k$ , $y_k = 1 + (-1)^{k+1}$ give $\limsup(x_k y_k) = 0 < 4$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 72 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Limit superior and limit inferior (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (standard reference, not scraped)
J. K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)

(−1)k(-1)^k(−1)k has lim inf⁡=−1\liminf = -1liminf=−1 and lim sup⁡=1\limsup = 1limsup=1, so it does not converge