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.

James space is isometrically isomorphic to its bidual

Statement

Assume Countable Choice. The James space $J$ is linearly isometric to its bidual $J^{* *}$ , although its canonical embedding is not onto.

Facts & Assumptions

[A1]

Countable Choice holds (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[L1]

Under Countable Choice, $J^{* *}$ is the max-of-cyclic-and-endpoint variation sequence space, and every element is a constant plus an element of $J$ (Dual and bidual models for James space).

Proof

technique · direct

Given: The objects and hypotheses in the Statement.

1.1

Define $T : J \to J^{* *}$ by $(T x)_{n} = x_{n + 1} - x_{1}$ for $n \geq 1$ . It is linear. If $p = (1 \leq p_{1} < \dots < p_{k})$ is a positive tuple, direct substitution gives

givenL1A1

$q_{p} (T x) = q_{(p_{1} + 1, \dots, p_{k} + 1)} (x), r_{p} (T x) = q_{(1, p_{1} + 1, \dots, p_{k} + 1)} (x) .$

Every tuple for $x$ either contains $1$ or, after shifting down, has one of these two forms. Therefore [L1] gives $∥ T x ∥_{J^{* *}} = ∥ x ∥_{J}$ ; in particular $T$ is injective. [A1, L1, direct calculation]

2.1

Let $z \in J^{* *}$ and set $λ = \lim_{n \to \infty} z_{n}$ , supplied by [given, L1, step 1.1] [L1]. Define $x_{1} = - λ$ and $x_{n + 1} = z_{n} - λ$ for $n \geq 1$ . Then $x_{n} \to 0$ , the identities in step 1.1 read backwards show $∥ x ∥_{J} = ∥ z ∥_{J^{* *}} < \infty$ , and $T x = z$ . Thus $T$ is surjective and is a linear isometry.

L1step 1.1

3.1

This $T$ is not the canonical embedding: by [L1] the latter misses the [given, L1, step 2.1] nonzero constant summand. Hence isometric isomorphism does not make $J$ reflexive.

L1step 1.12.1∎

Depends on

Used by

Nothing in the library uses this result yet.

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

Theo Bühler and Dietmar Salamon, Functional Analysis (standard reference, not scraped)