Alphabeta Math
False statementConstruction: AI-adaptedVerification: AI-generatedprecheck 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.

FALSE: a sequence with a convergent subsequence is bounded (the converse of Bolzano-Weierstrass)

Statement

False claim: if a sequence (yn) of reals has a convergent subsequence, then (yn) is bounded (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Subsequential limit of a real sequence, and the subsequential limit set).

This is the converse of Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence, which says that boundedness implies the existence of a convergent subsequence. The implication does not reverse, and it fails as badly as it can: a sequence can be unbounded and still have a constant subsequence.

The witness is the interleaving 1,1,2,1,3,1,4,…, in which the terms at even indices run through 1,2,3,… and every odd-indexed term is 1. It is recorded separately as the named counterexample of the companion page. The even and odd index maps are supplied by 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, which also supplies what makes the definition legitimate: every natural number is an even index or an odd index, and never both.

Facts & Assumptions

Given: The strictly increasing index maps e,o:N→N 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, whose ranges partition N, and the sequence (yn) of reals defined by cases on that partition: yn:=(j+1)⋅1R when n=ej, and yn:=1 when n=oj (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L2]

Canonical naturals: m⋅1R>0 for m≥1, and m↦m⋅1R is strictly increasing (Canonical naturals are positive and strictly increasing).

[L3]

Archimedean property: for every real x there is a natural m≥1 with x<m⋅1R (Every complete ordered field is Archimedean).

[L4]

Absolute value: ∣t∣≥t always, and ∣t∣=t when t≥0 (Basic properties of the absolute value).

[L5]

A constant sequence converges to its value, and a sequence is bounded when some real M satisfies ∣yn∣≤M at every index (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).

[L6]

Subsequences and subsequential limits: for strictly increasing n, (ynj) is a subsequence, and its limit is a subsequential limit of (yn) (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Subsequential limit of a real sequence, and the subsequential limit set).

[L8]

The refuted claim: a sequence of reals with a convergent subsequence is bounded.

Refutation

technique · direct
1.1

The sequence (yn) is well defined: by [L1] each n∈N falls under exactly one of the two clauses, and the index j realising it is unique, so exactly one value is assigned to each n.

givenL1
2.1

The subsequence along o is the constant sequence with value 1: for every j, yoj=1 by the second clause. Since o is strictly increasing, this is a subsequence of (yn).

step 1.1L1L6
2.2

The subsequence along e takes the value yej=(j+1)⋅1R for every j.

step 1.1L1
3.1

The constant subsequence (yoj) converges, to 1, so (yn) has a convergent subsequence and 1 is a subsequential limit of it: (yn) satisfies the hypothesis of the claim.

step 2.1L5L6L8
3.2

(yn) is not bounded. Let M∈R be arbitrary. By [L3] fix a natural m≥1 with ∣M∣<m⋅1R, and take j:=m−1∈N, which is legitimate since m≥1. Then yej=m⋅1R>∣M∣≥M, and yej>0 gives ∣yej∣=yej>M. So no real M satisfies ∣yn∣≤M at every index.

step 2.2L2L3L4L5L7
4.1

The sequence (yn) therefore has a convergent subsequence and is unbounded: the claim is false.

step 3.1step 3.2L8∎

Remarks

Depends on

Used by

Dependency tree · two levels

30 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