Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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.

Continuous dual of a weak topology

Statement

For a real or complex normed space X, the scalar-linear continuous dual of (X,σ(X,X∗)) is precisely X∗. No choice principle is required.

Facts & Assumptions

[F1]

Finite coordinate disks form a weak zero-neighborhood base (Basic weak neighborhoods).

[F2]

A scalar-linear map on a finite-dimensional normed space is bounded (A linear map from a finite-dimensional normed space is bounded).

Proof

Given: a weakly continuous scalar-linear L:X→K.

1.1F1given

Continuity at zero supplies f1,…,fm∈X∗ and ε>0 such that ∣L(v)∣<1 whenever max⁡j∣fj(v)∣<ε. If every fj(v)=0, every scalar multiple tv is in this neighborhood. Then ∣tL(v)∣<1 for all positive real t, forcing L(v)=0. For an empty list this already gives L=0.

2.1step 1.1algebra

Define A:X→Km by Av=(f1(v),…,fm(v)). Step 1.1 makes ℓ(Av)=L(v) a well-defined scalar-linear functional on A(X). Choose a basis of this subspace and extend it to a basis of Km by successively adding standard basis vectors when necessary; at most m additions occur. Assign value zero on the added basis vectors. The resulting linear extension ℓ~ has the form ℓ~(z)=∑j=1mcjzj, where cj=ℓ~(ej). Only finite-dimensional basis choices occur.

3.1step 2.1F2F1algebra

By finite-dimensional boundedness ℓ is bounded for the inherited norm, so factorization already gives norm boundedness of L. More explicitly L=∑jcjfj and ∣L(v)∣≤(∑j∣cj∣∥fj∥)∥v∥, hence L∈X∗. Conversely, for any f∈X∗ and any scalar disk around f(x), its inverse image is a basic weak neighborhood, so f is weakly continuous. Thus both inclusions hold. □

Depends on

Used by

Dependency tree · two levels

7 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