Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
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 sequentially compact metric space is complete, with no choice principle used

Statement

Let (X,d)(X,d) be a sequentially compact metric space (Countably compact, sequentially compact and limit point compact metric spaces, Metric space: d(x,y)=0d(x,y) = 0 iff x=yx = y, symmetry, and the triangle inequality; pseudometric and ultrametric). Then (X,d)(X,d) is complete (Complete metric space: every Cauchy sequence converges in the space).

The proof is a theorem of ZF: it instantiates two existential statements and selects nothing.

Facts & Assumptions

Given: A sequentially compact metric space (X,d)(X,d).

[L1]

(X,d)(X,d) is sequentially compact: every sequence in XX has a subsequence converging to a point of XX (Countably compact, sequentially compact and limit point compact metric spaces, Sequences of reals: bounded, eventually, frequently, tails, subsequences, Convergence of a sequence in a metric space: xk→xx_k \to x iff d(xk,x)→0d(x_k, x) \to 0 in R\mathbb{R}).

[L2]

(X,d)(X,d) is complete when every Cauchy sequence in XX converges to a point of XX (Complete metric space: every Cauchy sequence converges in the space, Cauchy sequence in a metric space).

[L3]

A Cauchy sequence with a subsequence converging to pp converges to pp itself (A Cauchy sequence in a metric space with a convergent subsequence converges to that subsequence’s limit).

Proof

technique · direct
1.1

Let (xk)(x_k) be a Cauchy sequence in (X,d)(X,d).

L2
2.1

By sequential compactness there is a strictly increasing index map j↦njj \mapsto n_j and a point p∈Xp \in X with xnj→px_{n_j} \to p in (X,d)(X,d).

L1step 1.1
3.1

Since (xk)(x_k) is Cauchy and one of its subsequences converges to pp, the whole sequence converges to pp, and p∈Xp \in X.

L3step 2.1
4.1

So every Cauchy sequence in (X,d)(X,d) converges in XX, that is (X,d)(X,d) is complete.

L2step 3.1∎

Remarks

The converse fails. A complete metric space need not be sequentially compact: R\mathbb{R} with its usual metric is complete, and the sequence xk=kx_k = k has no convergent subsequence, every subsequence being unbounded. What has to be added to completeness is total boundedness, and that pair is equivalent to compactness (A complete, totally bounded metric space is compact, proved from countable choice used exactly once, For a metric space, compact, countably compact, limit point compact, sequentially compact, and complete together with totally bounded are all equivalent, given countable choice and dependent choice).

Why this direction is free while the companion is not. Here the sequence is handed to the proof and sequential compactness hands back a subsequence: one object is produced, once. In A sequentially compact metric space is totally bounded, proved from the axiom of dependent choice a point has to be produced at every stage, each in terms of the points already produced, and that is where a choice principle enters the page.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 68 results over 14 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