Alphabeta Math
CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passverified 2026-08-08 (gpt-5.6-terra-codex-subscription)
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.

A sequence with lim sup⁡=+∞: the greatest subsequential limit exists only in R‾

Statement refuted

That The limit superior is itself a subsequential limit in R‾ and is the greatest one can be stated inside R: that for every sequence (xk) of reals the set SL⁡(x) of real subsequential limits (Subsequential limit of a real sequence, and the subsequential limit set) has a greatest element and that element is lim sup⁡kxk.

The witness below has a nonempty SL⁡(x) with a greatest element, so the failure is not that the real set is empty: it is that the greatest element of SL⁡(x) is 0 while lim sup⁡kxk=+∞. The dominant behaviour of the sequence is invisible to SL⁡(x) and is recorded only by SL⁡‾(x) (Convergence in R‾ and the extended subsequential limit set: L∈R‾ is an extended subsequential limit when some subsequence converges to L, or diverges to L=±∞).

Facts & Assumptions

Given: The alternating sequence (sk) and the index maps e,o of The even and odd index maps and the alternating sequence: strictly increasing e,o with N their disjoint union, and the unique (sk) with s0=1, sσ(k)=−sk, which satisfies ∣sk∣=1, s∘e≡1 and s∘o≡−1; the canonical naturals ι(k)=k⋅1R with ι(0)=0; and the sequence xk:=ι(k) when sk=1 and xk:=0 when sk=−1.

[L3]

The order on R‾ is total, +∞ is greatest, every real is <+∞ and >−∞, and the order restricts on R to the order of R (The extended real line R‾=R∪{−∞,+∞}, its order, and the arithmetic that is left undefined).

[L5]

Canonical naturals: ι is strictly increasing with ι(k)≥0, and for every real M there is a natural p≥1 with M<ι(p) (Canonical naturals are positive and strictly increasing, Every complete ordered field is Archimedean).

[L6]

A convergent sequence of reals is bounded, a limit is unique, and a sequence agreeing with a constant from some index on converges to that constant (Every convergent sequence is bounded, A sequence has at most one limit, Convergence depends only on the tail, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

Counterexample

technique · direct
1.1

Each sk is 1 or −1, so (xk) is a well-defined sequence of reals with xk≥0 for every k; moreover xej=ι(ej) and xoj=0 for every j.

givenL1L5L7
1.2

The subsequence along o is constantly 0, and o is strictly increasing, so 0∈SL⁡(x).

givenL1L4L6
2.1

For every n∈N the tail supremum sup⁡Tn(x) is +∞. Given a real M, take a natural p≥1 with M<ι(p) and an index j at least as large as both n and p; then ej≥j≥n, so xej=ι(ej)∈Tn(x), and ej≥j≥p gives ι(ej)≥ι(p)>M. So no real number bounds Tn(x) above, and the least upper bound in R‾ must be +∞.

step 1.1L1L2L3L5L7
3.1

Every real subsequential limit of (xk) equals 0. Let n be strictly increasing with xni→L∈R; the subsequence is then bounded, say ∣xni∣≤B for every i. Suppose sni=1 for arbitrarily large i: taking a natural p≥1 with B<ι(p) and such an index i≥p, we get xni=ι(ni)≥ι(i)≥ι(p)>B, contradicting the bound. So there is I with sni=−1, hence xni=0, for every i≥I; a sequence equal to 0 from an index on converges to 0, so L=0 by uniqueness of limits.

step 1.1step 2.1L1L4L5L6L7
4.1

Consequently lim sup⁡kxk is the greatest lower bound of the family {+∞}, namely +∞, while SL⁡(x)={0} by steps 1.2 and 3.1, whose greatest element is the real number 0. Since 0≠+∞, the refuted claim fails for this sequence.

step 2.1step 1.2step 3.1L2L3∎

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

62 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