Alphabeta Math
Pipeline-generated
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.

✓ 5 results · all verified · 4 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Baire Principles of Functional Analysis — Examples

1 · Prerequisites

2 · Summary

These examples show both the dense singular behaviour predicted by Baire category and the failures caused by dropping completeness.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Condensation of singularities

Example

Assume DC. Let X be Banach, let Y be normed, and let F⊆B(X,Y) be not uniformly bounded. Then singular vectors, those x with sup⁡T∈F∥Tx∥=∞, form a dense Gδ set.

Facts & Assumptions

Given: DC, X,Y,F as displayed, and failure of uniform boundedness.

Verification

technique · direct
1.1given
2.1step 1.1∎

Therefore every nonempty open ball contains a singular vector, which is the condensation assertion.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Uniform boundedness fails on the incomplete space c_00

Statement refuted

Pointwise bounded families on arbitrary normed spaces need not be uniformly operator-norm bounded.

Facts & Assumptions

Given: c00 with the supremum norm and fn(x)=nxn.

Counterexample

technique · direct
1.1given

Every fn is bounded and ∥fn∥=n by testing the nth unit vector.

1.2given

For fixed finitely supported x, fn(x)=0 for all sufficiently large n, so sup⁡n∣fn(x)∣<∞.

2.1step 1.1step 1.2∎

The partial sums of (2−k)k≥1 lie in c00 and are Cauchy in the sup norm but converge in its completion to a non-finitely-supported sequence. Thus the domain is incomplete and steps 1.1--1.2 refute the claim.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

A bounded bijection of incomplete normed spaces need not be open

Statement refuted

A bounded bijective linear map between arbitrary normed spaces need not be open.

Facts & Assumptions

Given: The identity I:(c00,∥⋅∥1)→(c00,∥⋅∥∞).

Counterexample

technique · direct
1.1given

Since ∥x∥∞≤∥x∥1, I is bounded and bijective.

1.2given

Its inverse is unbounded: for x(m)=(1/m,…,1/m,0,…), ∥x(m)∥∞=1/m but ∥x(m)∥1=1.

1.3given

The target is incomplete by Uniform boundedness fails on the incomplete space c_00. The partial sums of (2−k)k≥1 are also Cauchy in the ℓ1 norm but have no limit in c00, so the domain is incomplete as well.

2.1step 1.2∎

If I were open, its inverse would be continuous at 0, hence bounded by linearity, contradicting step 1.2.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-09-07Open item page →

A closed everywhere-defined graph need not be bounded without completeness

Statement refuted

Without completeness, a linear operator with closed everywhere-defined graph need not be bounded.

Facts & Assumptions

Given: I:(c00,∥⋅∥∞)→(c00,∥⋅∥1).

Counterexample

technique · direct
1.1given

The equal-coordinate vectors from A bounded bijection of incomplete normed spaces need not be open show that I is unbounded.

1.2given

If xk→x in sup norm and xk→y in ℓ1 norm, then every coordinate converges to both xj and yj, hence x=y.

2.1step 1.1step 1.2∎

Thus the graph is closed in the product norm (The graph of a linear operator with a linear domain), while step 1.1 shows the operator is unbounded.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Differentiation on C^1[0,1] is closed and unbounded in the supremum norm

Example

With supremum norms, D:C1[0,1]⊂C[0,1]→C[0,1], Df=f′, has closed graph but is unbounded.

Facts & Assumptions

Given: fn→f and fn′→g uniformly, with fn∈C1[0,1].

Verification

technique · direct
1.1given

Newton--Leibniz Newton–Leibniz needs only continuity on [a,b], differentiability on (a,b), and a Riemann-integrable extension of the interior derivative gives fn(t)−fn(0)=∫0tfn′(s) ds. Passing to uniform limits yields f(t)−f(0)=∫0tg(s) ds.

2.1step 1.1

Since g is continuous, the integral function is differentiable with derivative g; hence f∈C1 and Df=g. The graph (The graph of a linear operator with a linear domain) is closed.

3.1given∎

For integers n≥1, put fn(t)=sin⁡(nt)/n. Then ∥fn∥∞≤1/n whereas ∥Dfn∥∞=1, so D is unbounded.

Sources