Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge 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.

James nonreflexivity sequence separated from an annihilator

Statement

Assume the ultrafilter lemma, the Axiom of Dependent Choice (DC), and the relative Hahn–Banach principle HB. If a real Banach space X is not reflexive, then for every θ(0,1) there are a separable closed linear subspace MX and a sequence (xn)nN in BX such that

xn(m)0(mM)

and

dist ⁣(M,co{xn:nN})θ,

where M={wX:w(m)=0 for every mM} and co means finite convex hull.

Facts & Assumptions

Given: the ultrafilter lemma, DC, HB, a nonreflexive real Banach space X, and θ(0,1).

[F1]

Under the ultrafilter lemma, DC and HB, a Banach space is reflexive if and only if every norm-bounded sequence has a weakly convergent subsequence (Reflexivity is equivalent to weak subsequential compactness of bounded sequences). Its proof combines the weak compact unit-ball criterion (Reflexive iff unit ball weakly compact) with Eberlein–Šmulian (Eberlein–Šmulian theorem), whose compactness branch uses compact-Hausdorff Tychonoff under the ultrafilter lemma (Assuming the ultrafilter lemma, an arbitrary product of compact Hausdorff spaces is compact).

[F2]

Under HB, the norm-closed scalar span of a sequence in a Banach space is a separable Banach subspace, is weakly closed, and has intrinsic weak topology equal to its relative ambient weak topology (Eberlein–Šmulian separable reduction).

[F3]

Reflexivity is surjectivity of the canonical map, and under HB that map is a scalar-linear isometry (Reflexivity is surjectivity of the canonical map, Relative Hahn–Banach makes the canonical bidual map an isometry).

[F4]

DC is the entire-relation chain principle. Countable Choice ACω selects from a supplied sequence of nonempty sets (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain, The Axiom of Countable Choice (ACω)).

[F5]

Under ACω, a complete normed subspace of a normed space is closed (A complete normed subspace is closed under countable choice).

[F6]

A nonempty at most countable set admits a surjection from N; separability means having an at most countable dense subset (A nonempty set is at most countable iff it is a surjective image of N, Separability: the existence of an at most countable dense subset).

[F7]

Under HB, a bounded linear functional on any real linear subspace has an ambient extension of the same norm (Relative norm-preserving Hahn–Banach extension over the real and complex fields), derived from the relative dominated-extension principle (Dominated extension conditional on the relative principle, The real dominated-extension principle as an additional hypothesis over ZF).

[F8]

The dual norm is the supremum over the closed unit ball, and annihilators use the notation M={f:f(M)=0} (The dual space X^* of a normed space and its dual norm, Annihilator notation and the preannihilator).

Proof

Proof technique: separable reduction followed by finite annihilator duality and countable Hahn–Banach selection.

1.1

We first derive the exact Countable Choice instance used below. For a sequence (En) of nonempty sets, let S consist of all finite histories s with s(j)Ej for j<doms, starting with the empty history, and relate s to every one-term extension by a member of Edoms. This relation is entire. DC gives a chain of successively extended histories, whose union chooses one element of every En. Thus the assumed DC supplies every application of ACω below; we do not use the unproved bibliographic remark “DC implies ACω” as a theorem.

F4construct
1.2

By the contrapositive of [F1], choose a norm-bounded sequence (zn) in X with no weakly convergent subsequence. If R bounds all zn, then R>0, since an R=0 sequence is constantly zero. Replacing zn by zn/R, which preserves and reflects weak convergence of subsequences, we may assume znBX. Put M=spanR{zn:nN}. By [F2], M is a separable closed Banach subspace, and its intrinsic weak topology is the relative weak topology inherited from X.

F1F2algebra
2.1

The space M is not reflexive. Otherwise [F1], applied to the bounded sequence (zn) in the Banach space M, would give a subsequence converging weakly in M. Equality of the two weak topologies in [F2] would make the same subsequence weakly convergent in X, contrary to step 1.2. In particular M{0}.

step 1.2F1F2
3.1

Let JM:MM be the canonical map and Y=JM(M). By [F3], JM is an isometry, so Y is isometric to the complete space M. Step 1.1 and [F5] therefore make Y norm closed in M. It is proper because M is not reflexive.

step 1.1step 2.1F3F5
4.1

Choose qMY and put d=dist(q,Y). Closedness of Y gives d>0. Since d/θ>d and d is the infimum of the nonempty set {qy:yY}, choose yY with qy<d/θ. Define F=(qy)/qy. Then F=1, translation by yY does not change distance to the linear subspace Y, and hence dist(F,Y)=dqy>θ. No simultaneous family is chosen here.

step 3.1givenalgebrachoose
5.1

Since M is nonzero and separable, take a nonempty at most countable norm-dense subset DM and, by [F6], one surjection jmj from N onto D. Repetitions are harmless.

step 2.1step 4.1F6choose
6.1

For nN set Kn={uM:u(mj)=0 for 0jn},En=span{JMmj:0jn}. Then En=Kn inside M. The inclusion EnKn follows by evaluation. Conversely, if HM vanishes on Kn, define T:MRn+1 by T(u)=(u(m0),,u(mn)). Since kerT=Kn, the rule λ(Tu)=H(u) is a well-defined linear functional on imT. Finite-dimensional linear algebra extends λ to a functional (t0,,tn)j=0najtj on Rn+1, using only finitely many choices. Thus H=j=0najJMmjEn.

step 3.1step 5.1F3constructalgebra
7.1

The quotient-norm identity FKn=dist(F,En) holds. For HEn=Kn, restriction gives FHFKn. Conversely [F7] extends FKn to some GM with G=FKn; then FG vanishes on Kn, so step 6.1 puts FG in En and yields the reverse inequality. Since EnY, step 4.1 now gives FKn=dist(F,En)dist(F,Y)>θ.

step 4.1step 6.1F7F8
8.1

For each n, the last strict inequality and the dual-norm definition supply vKn with v1 and F(v)>θ. Replacing v by v if necessary and then setting u=θv/F(v) gives uKn, u<1, and F(u)=θ. By [F7], u has an extension xX with x=u<1. Therefore the set Pn of all such pairs (u,x) is nonempty.

step 7.1F7F8algebra
9.1

Apply the ACω instance from step 1.1 to (Pn), writing the selected pair as (un,xn). Then xnBX, xnM=un, F(un)=θ, and un(mj)=0 whenever jn. For fixed mM and ε>0, density supplies mj with mmj<ε; for nj, xn(m)=un(mmj)unmmj<ε. Hence xn(m)0 for every mM.

step 1.1step 5.1step 8.1F6
10.1

Let x=k=1rakxnk be any finite convex combination, where r1, ak0, and kak=1, and let wM. Restriction to M and step 9.1 give F ⁣((xw)M)=k=1rakF(unk)=θ. Since F=1, restriction cannot increase norm, and therefore xw(xw)Mθ. Taking the infimum over both nonempty sets proves dist(M,co{xn:nN})θ.

step 4.1step 9.1F8algebra
11.1

Steps 1.2 and 2.1 provide the required separable closed M, step 9.1 gives the pointwise-null dual-ball sequence, and step 10.1 gives the asserted annihilator separation. The endpoints θ=0,1 are excluded exactly as stated; X={0} cannot satisfy the nonreflexivity hypothesis. The argument is real: the sign change and the order comparison in step 8.1 are not offered as a complex proof. The ultrafilter lemma and HB enter through [F1], HB also enters through [F2], [F3] and [F7], and DC enters exactly through the finite-history derivation in step 1.1.

step 1.1step 1.2step 2.1step 9.1step 10.1F1F2F3F7

Source notes

Megginson's Theorem 1.13.11(a)→(b), printed pp. 125–126, supplies the separable finite-test bidual construction. Theorem 1.13.14(a)→(b), printed p. 132, first reduces an arbitrary nonreflexive real Banach space to a separable closed nonreflexive subspace and then extends the resulting functionals to the ambient space. The proof above expands the finite annihilator identity and records every choice principle used.

Depends on

Used by

Dependency tree · two levels

70 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