Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14
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.

Dvoretzky--Rogers theorem

Statement

Assume Countable Choice. Every infinite-dimensional real or complex Banach space contains an unconditionally convergent series that is not absolutely convergent.

Facts & Assumptions

[A1]
[L1]

Each sufficiently high-dimensional finite block admits vectors with prescribed squared norms and the uniform subset-sum estimate (The Dvoretzky--Rogers finite-block estimate).

[L2]

Uniform smallness of all finite tails is equivalent to unconditional convergence in a Banach space (Equivalent forms of unconditional convergence).

Proof

technique · construction

Given: The objects and hypotheses in the Statement.

1.1

Put cn=(8n2)1 for n1. Since n1n2<2, we have ncn<1/4, while ncn=81/2n1/n=. Put N1=1 and, for m2, recursively take Nm to be the least integer greater than Nm1 such that nNmcn<4m. Thus

given

m(Nmn<Nm+1cn)1/2<.

[explicit least-index recursion, scalar series]

2.1

Let rm=Nm+1Nm. Infinite-dimensionality supplies a subspace of dimension at least rm(rm1) (the cases rm1 are chosen directly). Use [A1] exactly here to select, for all m, one family (xn)Nmn<Nm+1 given by [L1] with dn=cn. Then xn=1/(8n) and every subset F of the mth block satisfies

givenA1L1step 1.1

nFxn3(nFcn)1/2.

[A1, L1, step 1.1]

3.1

For any finite set F contained in the tail beginning at NM, split it by blocks and use the triangle inequality and step 2.1:

givenL2step 2.1step 1.1

nFxn3mM(Nmn<Nm+1cn)1/2.

The right side tends to zero by step 1.1. Condition (3) of [L2] therefore holds, so nxn converges unconditionally. [L2, steps 1.1, 2.1]

4.1

On the other hand, [given, step 2.1, step 3.1] nxn=81/2n1/n=, so the same series is not absolutely convergent.

step 2.1algebra

Depends on

Used by

Dependency tree · two levels

11 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