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.

10 results · all verified · 10 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; all 10 also cleared it.

The Analytic Hahn Banach Theorem

1 · Prerequisites

2 · Summary

This page follows the analytic route through Hahn-Banach. It starts with sublinear domination, isolates the one-step interval calculation and the chain-union upper bound needed for Zorn, and then proves the real dominated extension theorem. It next packages the normed-space consequences: the dual space, norm-preserving extension in the real and complex cases, norming functionals, separation by the dual, and recovery of the norm from the dual unit ball.

The page also keeps one boundary explicit: the norm-preserving extension theorem does not require the domain subspace to be closed. Seminorms, geometric separation, and finite-dimensional complementation are deliberately left to the next functional-analysis page.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

A sublinear functional on a real vector space

Definition

Let X be a real vector space (Vector space over a field). A function p:XR is a sublinear functional if

p(x+y)p(x)+p(y)for all x,yX,

and

p(tx)=tp(x)for all xX and all t0.

Remarks

  • Taking t=0 shows p(0)=0.
  • No condition is imposed for negative scalars beyond what follows from the two displayed axioms.
  • A norm on a real vector space is sublinear, but a sublinear functional need not be symmetric: in general one can have p(x)p(x).
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

The admissible values in a one-step Hahn-Banach extension form a nonempty interval

Statement

Let X be a real vector space, let MX be a linear subspace, let p:XR be sublinear, and let f:MR be linear with f(m)p(m) for every mM. Fix x0XM and put N:=M+Rx0.

For cR define

Fc(m+tx0):=f(m)+tc(mM, tR).

This is well defined, and with

α:=supyM(f(y)p(yx0)),β:=infzM(p(z+x0)f(z)),

one has αβ. Moreover, Fc(n)p(n) for every nN if and only if αcβ. In particular the admissible values of Fc(x0)=c form the nonempty interval [α,β].

Facts & Assumptions

Given: A real vector space X, a linear subspace MX, a sublinear functional p:XR, a linear functional f:MR with fp on M, and a point x0XM.

[L1]

A sublinear functional satisfies p(u+v)p(u)+p(v) and p(tu)=tp(u) for every real t0 (A sublinear functional on a real vector space).

[L2]

A linear functional is additive and homogeneous over the scalar field (Linear functionals and the algebraic dual V=L(V,F)).

[L3]

A linear subspace is closed under addition and scalar multiplication (Linear subspace of a vector space).

Proof

technique · direct
1.1

If m+tx0=m+tx0 with m,mM and t,tR, then mm=(tt)x0M. If tt, closure under scalar multiplication from [L3] gives x0M, contradicting the hypothesis. So t=t and then m=m. Therefore every element of N has a unique representation m+tx0, and Fc is well defined.

L3givenconstruct
1.2

For y,zM, one has Fc(yx0)=f(y)candFc(z+x0)=f(z)+c. Therefore Fc(yx0)p(yx0)    f(y)p(yx0)c, and Fc(z+x0)p(z+x0)    cp(z+x0)f(z).

L2givenalgebra
1.3

Let y,zM. Since y+zM by [L3], linearity and domination on M give f(y)+f(z)=f(y+z)p(y+z). Also y+z=(yx0)+(z+x0), so subadditivity from [L1] yields p(y+z)p(yx0)+p(z+x0). Combining these inequalities gives f(y)p(yx0)p(z+x0)f(z). Hence every lower endpoint is at most every upper endpoint.

L1L2L3givenalgebra
2.1

Suppose first that the two inequalities from step 1.2 hold for every y,zM. Let m+tx0N. If t>0, then m+tx0=t(mt+x0), so by linearity and positive homogeneity, Fc(m+tx0)=tFc(mt+x0)tp(mt+x0)=p(m+tx0). If t<0, then m+tx0=(t)(mtx0), so the lower-bound half of step 1.2 applied to y:=m/t gives Fc(m+tx0)=(t)Fc(mtx0)(t)p(mtx0)=p(m+tx0). If t=0, then m+tx0=mM, so the hypothesis fp gives Fc(m)=f(m)p(m). Thus Fcp on N. Conversely, if Fcp on N, then applying that inequality to yx0 and z+x0 yields the two inequalities in step 1.2.

step 1.2L1L2givenalgebra
3.1

Step 1.3 shows that the set of lower endpoints is bounded above by every upper endpoint, and the set of upper endpoints is bounded below by every lower endpoint. Completeness of R therefore gives real numbers αβ with the displayed formulas in the statement. By step 2.1, a real number c is admissible exactly when it lies between every lower endpoint and every upper endpoint, that is, exactly when αcβ. Therefore the admissible values form the nonempty interval [α,β].

step 2.1step 1.3
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

The union of a chain of dominated extensions is a well-defined dominated linear functional

Statement

Let X be a real vector space and let p:XR be sublinear. Let C be a nonempty chain, ordered by extension, of pairs (N,g) such that NX is a linear subspace and g:NR is linear with g(n)p(n) for every nN.

Put

U:=(N,g)CN.

Then U is a linear subspace of X, and the pointwise union G:UR defined by G(x)=g(x) whenever xN is a well-defined linear functional with G(u)p(u) for every uU.

If every (N,g)C extends the same linear functional f:MR, then G also extends f.

Facts & Assumptions

Given: A real vector space X, a sublinear functional p:XR, and a nonempty chain C of dominated linear functionals ordered by extension.

[L1]

A linear functional is additive and homogeneous over the scalar field (Linear functionals and the algebraic dual V=L(V,F)).

[L2]

A chain is a subset in which any two elements are comparable (Chain in a poset).

Proof

technique · direct
1.1

If xN1N2 for (N1,g1),(N2,g2)C, then [L2] gives comparability. Suppose N1N2. Since the chain order is extension, g2N1=g1, so g1(x)=g2(x). The other inclusion case is the same. Therefore G(x) is well defined on overlaps.

L2givenconstruct
1.2

Let u,vU and aR. Choose (N1,g1),(N2,g2)C with uN1 and vN2. By [L2], one of the domains contains the other; after relabeling, assume N1N2. Then u,vN2, so u+vN2 and auN2 because N2 is a linear subspace. Hence u+v,auU. Thus U is a linear subspace.

L2givenalgebra
2.1

With the same choice of N2 as in step 1.2, one has G(u+v)=g2(u+v)=g2(u)+g2(v)=G(u)+G(v), and G(au)=g2(au)=ag2(u)=aG(u), by [L1]. Therefore G is linear.

step 1.1step 1.2L1
3.1

If uU, choose (N,g)C with uN. Then G(u)=g(u)p(u) by the defining property of the chain element, so G is dominated by p. If every chain element extends the same f:MR, then every mM lies in each domain and all values there equal f(m), so GM=f.

step 1.1given
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

Hahn-Banach dominated extension theorem for real vector spaces

Statement

Assume the Axiom of Choice. Let X be a real vector space, let MX be a linear subspace, let p:XR be sublinear, and let f:MR be linear with f(m)p(m) for every mM. Then there exists a linear functional F:XR such that FM=f and F(x)p(x) for every xX.

Facts & Assumptions

Given: The Axiom of Choice, a real vector space X, a linear subspace MX, a sublinear functional p:XR, and a linear functional f:MR with fp on M.

[L1]

The one-step extension problem over M+Rx0 has a nonempty interval of admissible values for F(x0) (The admissible values in a one-step Hahn-Banach extension form a nonempty interval).

[L2]

The union of a chain of dominated extensions is again a well-defined dominated extension (The union of a chain of dominated extensions is a well-defined dominated linear functional).

[L3]

Assuming the Axiom of Choice, a nonempty poset in which every chain has an upper bound has a maximal element (Zorn's lemma).

Proof

technique · direct
1.1

Let E be the set of all pairs (N,g) such that MNX, the set N is a linear subspace of X, the map g:NR is linear, gM=f, and gp on N. Order E by extension: (N1,g1)(N2,g2)    N1N2 and g2N1=g1. The pair (M,f) lies in E, so this poset is nonempty.

givenconstruct
2.1

Let CE be a chain. If C=, then (M,f) is an upper bound for it. If C, [L2] applies to the union of its domains and yields a well-defined linear functional dominated by p; because every chain element extends f, that union functional still extends f. Hence every chain in E has an upper bound in E.

L2step 1.1given
3.1

By [L3], choose a maximal element (N,F) of E. If NX, choose x0XN. Applying [L1] to the dominated functional F on the subspace N produces a dominated linear extension F~ on N+Rx0. Then (N,F)(N+Rx0,F~), contradicting maximality. Therefore N=X.

L1L3step 2.1choose
4.1

Since the maximal domain is all of X, the corresponding functional F is the required dominated extension of f.

step 3.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

The dual space X^* of a normed space and its dual norm

Definition

Let X be a normed space over the scalar field K, where K=R in the literal definition and K=C by the convention of Real and complex scalar conventions for normed spaces. The dual space of X is

X:=B(X,K),

the space of bounded linear functionals on X (The spaces (\mathcal B(X,Y)) and (\mathcal B(X)) of bounded linear operators).

Each fX is in particular a linear functional in the algebraic sense, so X is a subspace of the algebraic dual from Linear functionals and the algebraic dual V=L(V,F).

The dual norm on X is the operator norm:

fX:=f=sup{f(x):x1}.

Remarks

  • The pairing between X and X is evaluation: (f,x)f(x).
  • In this library, X means the topological dual unless the phrase "algebraic dual" is written explicitly.
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

A bounded real linear functional on a subspace of a real normed space extends with the same norm

Statement

Let X be a real normed space, let MX be a linear subspace, and let f0:MR be a bounded linear functional. Then there exists a bounded linear functional F:XR such that FM=f0 and F=f0.

Facts & Assumptions

Given: A real normed space X, a linear subspace MX, and a bounded real linear functional f0:MR.

[L1]

A dominated real linear functional extends to the whole real vector space (Hahn-Banach dominated extension theorem for real vector spaces).

[L2]

A bounded linear operator has some constant C0 with TxCx for every x (A bounded linear operator between normed spaces).

[L3]

The operator norm is the least such bound: T=inf{C0:TxCx for all x} (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[L4]

A normed subspace carries the restricted norm from the ambient space (Normed subspace).

Proof

technique · direct
1.1

Define p:XR by p(x):=f0x. The triangle inequality and real homogeneity of the norm make p sublinear. For mM, [L3] and [L4] give f0(m)f0(m)f0m=p(m), so f0p on M.

L3L4givenconstructalgebra
2.1

By [L1], there exists a linear functional F:XR extending f0 and satisfying F(x)p(x) for every xX.

L1step 1.1
3.1

Apply step 2.1 to x and to x. Since p(x)=p(x), one gets f0xF(x)f0x, hence F(x)f0x(xX). So F is bounded in the sense of [L2], and [L3] gives Ff0.

step 2.1L2L3algebra
3.2

Since FM=f0, for every mM with m1 one has f0(m)=F(m)F. Taking the supremum over the unit ball of the normed subspace M and using [L3] and [L4] yields f0F.

step 2.1L3L4
4.1

Steps 3.1 and 3.2 give F=f0, so F is the required norm-preserving extension.

step 3.1step 3.2
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

A complex linear functional is recovered from its real part by f(x)=u(x)-iu(ix)

Statement

Let X be a complex vector space.

If f:XC is complex linear and u:=Ref, then u is real linear on the underlying real vector space and

f(x)=u(x)iu(ix)(xX).

Conversely, if u:XR is real linear on the underlying real vector space, then

g(x):=u(x)iu(ix)(xX)

defines a complex linear functional with Reg=u. In particular a complex linear functional is uniquely determined by its real part.

Facts & Assumptions

Given: A complex vector space X, a complex linear functional f:XC, and a real linear functional u on the underlying real vector space.

[L1]

A linear functional is additive and homogeneous over the relevant scalar field (Linear functionals and the algebraic dual V=L(V,F)).

[L2]

On this page, complex vector-space language is read by the scalar convention recorded in Real and complex scalar conventions for normed spaces.

Proof

technique · direct
1.1

Let u:=Ref. For x,yX and aR, u(x+y)=Re(f(x+y))=Ref(x)+Ref(y), and u(ax)=Re(f(ax))=Re(af(x))=au(x). So u is real linear.

L1L2givenalgebra
1.2

Write f(x)=a+ib with a,bR. Since f is complex linear, f(ix)=if(x)=iab, so Ref(x)=a and Ref(ix)=b. Therefore u(x)iu(ix)=ai(b)=a+ib=f(x).

L1givenalgebra
1.3

Conversely, let u be real linear and define g(x):=u(x)iu(ix). Additivity is immediate from real linearity of u. Also g(ix)=u(ix)iu(i2x)=u(ix)+iu(x)=i(u(x)iu(ix))=ig(x). Now for λ=a+ibC with a,bR, g(λx)=g(ax+bix)=ag(x)+bg(ix)=ag(x)+big(x)=λg(x). Hence g is complex linear.

L1L2givenconstructalgebra
2.1

Taking real parts in the definition of g gives Reg(x)=u(x) for every x. Together with step 1.2, this shows that a complex linear functional is uniquely determined by its real part.

step 1.2step 1.3algebra
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

A bounded complex linear functional on a subspace of a complex normed space extends with the same norm

Statement

Let X be a complex normed space, let MX be a linear subspace, and let f0:MC be a bounded complex linear functional. Then there exists a bounded complex linear functional F:XC such that FM=f0 and F=f0.

Facts & Assumptions

Given: A complex normed space X, a linear subspace MX, and a bounded complex linear functional f0:MC.

[L1]

A bounded real linear functional on a real normed subspace extends with the same norm (A bounded real linear functional on a subspace of a real normed space extends with the same norm).

[L2]

A complex linear functional is recovered from its real part by f(x)=u(x)iu(ix), and conversely every such formula defines a complex linear functional (A complex linear functional is recovered from its real part by f(x)=u(x)-iu(ix)).

[L3]

The complex case uses the scalar convention from Real and complex scalar conventions for normed spaces.

Proof

technique · direct
1.1

Let u:=Ref0. By [L2], u is real linear on the underlying real subspace M. Also u(m)f0(m)f0m(mM), so u is bounded with uf0.

L2givenalgebra
2.1

Apply [L1] to the underlying real normed spaces. This yields a bounded real linear functional U:XR extending u and satisfying U=u. Define F(x):=U(x)iU(ix)(xX). By [L2], F is complex linear and ReF=U.

L1L2step 1.1construct
3.1

For mM, the equality UM=u and [L2] give F(m)=u(m)iu(im)=f0(m). So F extends f0.

L2step 2.1
3.2

Fix xX. Choose θR so that eiθF(x)=F(x) is a nonnegative real number. Since ReF=U and F is complex linear, F(x)=Re(eiθF(x))=ReF(eiθx)=U(eiθx). Therefore F(x)Ueiθx=Uxf0x, where the last inequality uses step 1.1 and U=u. Hence Ff0.

L2L3step 1.1step 2.1choosealgebra
4.1

Since FM=f0, every mM with m1 satisfies f0(m)=F(m)F. Taking the supremum over the unit ball of M gives f0F. Combined with step 3.2, this yields F=f0.

step 3.1step 3.2algebra
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

Every nonzero vector has a norming functional

Statement

Let X be a normed space over R or C, and let xX be nonzero. Then there exists fX such that

f=1andf(x)=x.

Facts & Assumptions

Given: A normed space X over R or C and a vector xX with x0.

[L1]

The dual space X is the space of bounded linear functionals on X (The dual space X^* of a normed space and its dual norm).

[L2]

In the real case, a bounded linear functional extends with the same norm (A bounded real linear functional on a subspace of a real normed space extends with the same norm).

[L3]

In the complex case, a bounded linear functional extends with the same norm (A bounded complex linear functional on a subspace of a complex normed space extends with the same norm).

Proof

technique · direct
1.1

Let M:=span{x}. Define f0:MR or f0:MC by f0(λx):=λx. Because x0, each vector of M has a unique representation λx. Moreover, f0(λx)=λx=λx, so f0 is bounded and f0=1.

givenconstructalgebra
2.1

If the scalar field is R, [L2] extends f0 to a bounded real linear functional f on X with f=f0=1. Since x=1x, f(x)=f0(x)=x.

L2step 1.1
2.2

If the scalar field is C, [L3] extends f0 to a bounded complex linear functional f on X with f=f0=1. Again f(x)=f0(x)=x.

L3step 1.1
3.1

In either scalar case, the extension produced in step 2.1 or step 2.2 is a bounded linear functional on X, hence an element of X by [L1], with norm 1 and value x at x.

L1step 2.1step 2.2
CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

The dual space separates points of a normed space

Statement

Let X be a normed space over R or C. If x,yX with xy, then there exists fX such that f(x)f(y).

Facts & Assumptions

Given: A normed space X over R or C and two vectors x,yX with xy.

[L1]

Every nonzero vector admits a norming functional (Every nonzero vector has a norming functional).

Proof

technique · direct
1.1

Since xy, the vector xy is nonzero.

given
2.1

By [L1], there exists fX with f(xy)=xy. In particular f(xy)0.

L1step 1.1
3.1

If f(x)=f(y), then linearity would give f(xy)=0, contradicting step 2.1. Therefore f(x)f(y), so the dual space separates x and y.

step 2.1algebra
CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

The norm of a vector is the supremum of |f(x)| over the dual unit ball

Statement

Let X be a normed space over R or C. Then for every xX,

x=sup{f(x):fX, f1}.

Facts & Assumptions

Given: A normed space X over R or C and a vector xX.

[L1]

The dual norm on X is the operator norm, so f(x)fx for every fX (The dual space X^* of a normed space and its dual norm).

[L2]

Every nonzero vector admits a norming functional (Every nonzero vector has a norming functional).

Proof

technique · direct
1.1

If fX and f1, then [L1] gives f(x)fxx. So the displayed supremum is at most x.

L1given
2.1

If x=0, step 1.1 already shows that the supremum is 0, so the formula holds. Assume now that x0. By [L2], choose gX with g=1 and g(x)=x. Then the displayed supremum is at least g(x)=x.

L2givenchoose
3.1

Step 1.1 gives an upper bound of x, and step 2.1 gives equality. So x=sup{f(x):fX, f1}.

step 1.1step 2.1
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

A bounded linear functional on an arbitrary subspace extends with the same norm, without assuming the subspace is closed

Statement

Let X be a normed space over R or C, let MX be a linear subspace, and let f0:MR or f0:MC be a bounded linear functional over the ambient scalar field. Then there exists a bounded linear extension F of f0 to all of X such that F=f0.

No closedness hypothesis on M is needed.

Facts & Assumptions

Given: A normed space X over R or C, a linear subspace MX, and a bounded linear functional f0 on M.

[L1]

In the real case, a bounded linear functional on a subspace extends with the same norm (A bounded real linear functional on a subspace of a real normed space extends with the same norm).

[L2]

In the complex case, a bounded linear functional on a subspace extends with the same norm (A bounded complex linear functional on a subspace of a complex normed space extends with the same norm).

[L3]

The page's normed-space language is read over either scalar field by the convention of Real and complex scalar conventions for normed spaces.

Proof

technique · direct
1.1

If the scalar field is R, then [L1] applies exactly as stated to the given subspace M and produces a norm-preserving extension of f0 to X.

L1L3given
1.2

If the scalar field is C, then [L2] applies exactly as stated to the given subspace M and produces a norm-preserving extension of f0 to X.

L2L3given
2.1

Neither step 1.1 nor step 1.2 uses or requires that M be closed; each cited theorem assumes only that M is a linear subspace. Therefore every bounded linear functional on an arbitrary subspace extends with the same norm.

step 1.1step 1.2L1L2
RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-05 rests on unproved materialOpen item page →
Rests on 1 statement not proved in this library. Every dependency marked below is recorded with a citation but 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 set-theoretic cost of Hahn-Banach

Remark

The proof of Hahn-Banach dominated extension theorem for real vector spaces on this page is a Zorn proof, so that proof route uses the Axiom of Choice through Zorn's lemma. That is a proof cost, not the exact cost of the theorem itself.

The sharper ledger is recorded in The set-theoretic cost of Hahn-Banach . For the reader of this page, the key points are these:

So later pages should cite Hahn-Banach itself when they use the extension theorem, and should cite Zorn only when they really use this maximal-extension implementation.

5 · Examples, counterexamples and false statements

None yet.

Sources