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

6 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 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Finite Dimensional Normed Spaces and Riesz Lemma — Examples

1 · Prerequisites

2 · Summary

The companion page keeps the FA-3 results concrete: explicit norm constants, the separated-sphere witness from Riesz's lemma, a standard Heine-Borel failure in 2, the polynomial-space obstruction to completeness, an explicit three-point Kuratowski embedding, and the contrast between discontinuous functionals on incomplete spaces and the choice-sensitive Banach-space story.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-04Open item page →

Explicit comparison constants for the standard norms on K^n

Example

Let K{R,C} and let x=(x0,,xn1)Kn with n1. Define

x:=maxj<nxj,x2:=(j<nxj2)1/2,x1:=j<nxj.

Then

xx2x1nx2nx.

In particular, the abstract norm-equivalence theorems on the A page can be read with explicit constants on these three standard coordinate norms.

Facts & Assumptions

Given: A field K{R,C}, an integer n1, and a vector xKn.

[L1]

On Rn, the displayed 1, Euclidean, and max formulas are the standard norms of The p-norms xp for rational p1, and x, and every norm on Rn is equivalent to every other (For n1 all norms on Rn are equivalent).

[L2]

On finite-dimensional complex spaces every two norms are equivalent (All norms on a finite-dimensional complex normed space are equivalent).

Verification

technique · direct
1.1

Since every summand xj2 is nonnegative and one of them equals x2, one has x2j<nxj2=x22, hence xx2. Also x22=j<nxj2(j<nxj)2=x12, so x2x1.

L1algebra
2.1

By Cauchy-Schwarz for the vectors (xj)j<n and (1,,1), x1=j<nxj(j<nxj2)1/2(j<n12)1/2=nx2. Also xjx for every j, so x1nx.

step 1.1algebra
3.1

Combining steps 1.1 and 2.1 yields the displayed chain. Thus [L1] and [L2] become concrete on these coordinate norms.

L1L2step 1.1step 2.1

Remarks

  • The constants are sharp in the standard basis: x=(1,,1) makes x1=nx and x1=nx2.
ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

An infinite separated subset of the unit sphere

Example

Assume Dependent Choice. Let X be a normed space that is not the span of any finite list. Then the unit sphere of X contains an infinite subset whose distinct points are all more than 1/2 apart.

Facts & Assumptions

Given: Dependent Choice and a normed space X that is not the span of any finite list.

[L1]

Under these hypotheses, for every 0<α<1 there is a sequence of unit vectors (xn) with xnxm>α for nm (Under dependent choice, Riesz lemma builds an infinite separated sequence in the unit sphere).

Verification

technique · direct
1.1

Apply [L1] with α=1/2. This gives a sequence (xn) of unit vectors such that xnxm>1/2 whenever nm.

L1
2.1

The set {xn:nN} is therefore an infinite subset of the unit sphere whose distinct points are pairwise more than 1/2 apart.

step 1.1
CounterexampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Heine-Borel fails in ell^2

Statement refuted

Refuted claim: every closed and bounded subset of an infinite-dimensional Banach space is compact.

Take the Hilbert space

2:={x=(xn)n0:n=0xn2<}.

Its closed unit ball is closed and bounded, but it is not compact.

Facts & Assumptions

Given: The space 2, its standard unit vectors en, and its closed unit ball B2.

[L1]

In any normed space with no ordered basis of finite length, the closed unit ball is not compact (In an infinite-dimensional normed space the closed unit ball is not compact).

[L2]

The classical sequence spaces p are Banach; in particular 2 is Banach (The classical Lp spaces are Banach spaces).

Counterexample

technique · direct
1.1

The standard unit vectors are linearly independent: if j=0majej=0, then the j-th coordinate of that sequence is aj, so every aj=0. Therefore the set {en:nN} is linearly independent and is equinumerous with N. By [L3], 2 cannot be spanned by any finite list, hence it admits no ordered basis of finite length. Each en belongs to 2 and has norm 1, so every en lies in the closed unit ball. Also for mn one has enem2=2.

L3givenalgebra
2.1

By [L2], 2 is a Banach space. Since step 1.1 shows that 2 admits no ordered basis of finite length, [L1] implies that B2 is not compact. This closed unit ball is closed and bounded by definition, so it refutes the claim.

L1L2step 1.1

Remarks

  • The Banach-space adjective in the refuted claim is there because the failure is not an incompleteness issue. The obstruction is infinite dimension.
CounterexampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04 rests on unproved material (inherited)Open item page →
Rests on 1 statement not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are The Baire category theorem is four inequivalent statements over ZF. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

The polynomial space admits no complete norm

Statement refuted

Refuted claim: the polynomial space over a scalar field can be made into a Banach space by some norm.

Let K{R,C} and let K[x] be the polynomial ring of The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution, regarded as a vector space over K. Then no norm on K[x] is complete.

Facts & Assumptions

Given: A scalar field K{R,C} and the vector space K[x] of polynomials in one indeterminate.

[L1]

A Banach space has no countably infinite Hamel basis (A Banach space has no countably infinite Hamel basis).

[L3]

The polynomial ring K[x] is the set of finite sums a0+a1x++amxm (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

Counterexample

technique · direct
1.1

The set {1,x,x2,} spans K[x] by [L3], because every polynomial is a finite linear combination of monomials. It is linearly independent: if a0+a1x++amxm=0 as a polynomial, then every coefficient is 0. Hence [L2] makes {1,x,x2,} a countably infinite Hamel basis of K[x].

L2L3algebra
2.1

If some norm on K[x] were complete, then [L1] would forbid the countably infinite Hamel basis from step 1.1. This contradiction shows that no norm on K[x] is complete.

L1step 1.1assume-contradischarge-contradiction
ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

The Kuratowski embedding of a finite metric space

Example

Let M={o,a,b} with metric determined by

d(o,a)=1,d(a,b)=1,d(o,b)=2.

Using o as basepoint, the based Kuratowski map Ko:MCb(M) is given by

Ko(o)=(0,0,0),Ko(a)=(1,1,1),Ko(b)=(2,0,2),

where each function is recorded by its values on (o,a,b). These three points in R3 are at the same pairwise sup distances as the original metric space.

Facts & Assumptions

Given: The three-point metric space M={o,a,b} above.

[L1]

The based Kuratowski map preserves all distances (The based Kuratowski distance map is an isometric embedding).

Verification

technique · direct
1.1

By definition, Ko(x)(z)=d(x,z)d(o,z). Evaluating this on the three points gives Ko(o)=(0,0,0), Ko(a)=(1,1,1), and Ko(b)=(2,0,2).

givenalgebra
2.1

The sup distances are Ko(a)Ko(o)=1, Ko(b)Ko(a)=1, and Ko(b)Ko(o)=2, exactly matching d(o,a), d(a,b), and d(o,b). This is the concrete instance promised by [L1].

L1step 1.1algebra
RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Discontinuous linear functionals on infinite-dimensional Banach spaces are not available in ZF + DC

Remark

On an infinite-dimensional Banach space, the existence of a discontinuous linear functional is a choice-sensitive statement. Full Choice gives one immediately from an infinite Hamel basis: pick the basis, prescribe an unbounded coefficient functional on it, and extend linearly. The opposite direction is not a theorem of ZF + DC. Howard and Tachtsis record the consistency boundary, and Heil's discussion of Hamel bases spells out the elementary "basis gives an unbounded functional" half.

The point for this page is negative rather than positive: the explicit discontinuous functional on the companion example below lives on the incomplete space c00, not on a Banach space. That distinction is exactly why this remark is kept separate from the example and why it never serves as a dependency.

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-04Open item page →

A choice-free discontinuous linear functional on c_00

Example

Let

c00:={x=(xn)n0:xn=0 for all but finitely many n}

with the supremum norm x:=supnxn, a norm in the sense of A norm on a real vector space, the induced metric, and the dictionary with the metric axioms. Define

f:c00R,f(x):=n=0(n+1)xn.

Because every xc00 has finite support, the displayed sum is really finite. The map f is linear but unbounded, hence discontinuous.

Facts & Assumptions

Given: The space c00 with its supremum norm and the standard unit vectors en.

[L1]

Linearity means preserving scalar combinations (Linear map between vector spaces over the same field).

Verification

technique · direct
1.1

Because every element of c00 has finite support, the displayed sum for f(x) has only finitely many nonzero terms. Therefore f is well defined, and termwise addition shows f(ax+by)=af(x)+bf(y) for all scalars a,b and all x,yc00. Thus f is linear by [L1].

L1L2algebra
2.1

For each n, the unit vector en satisfies en=1 and f(en)=n+1. Hence the values of f on the unit sphere are unbounded, so no constant C can satisfy f(x)Cx for all xc00. Thus f is unbounded.

step 1.1algebra
3.1

Every bounded linear functional on a normed space is continuous at 0, so an unbounded linear functional cannot be continuous. Therefore f is a discontinuous linear functional on c00.

step 2.1assume-contradischarge-contradiction

Remarks

  • This is the explicit incomplete-space witness promised by the companion remark. No choice principle is used anywhere in the construction.

Sources