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.

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

Geometric Hahn Banach and Convex Separation

1 · Prerequisites

2 · Summary

The gauge turns a translated open convex neighbourhood into a real sublinear functional. Under the Axiom of Choice, Hahn–Banach supplies geometric separation, with real parts used over complex scalars. The later results apply separation to subspace closure, complemented finite-dimensional directions, and weak/norm closure of convex sets. The closed-hyperplane theorem has a separate choice-free proof using the coefficient along one complementary vector.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableOpen item page →

Absorbing, balanced, and absolutely convex sets

Definition

Let X be a normed space over K∈{R,C}, with the real norm definition A norm on a real vector space, the induced metric, and the dictionary with the metric axioms over R and the complex norm definition Complex norm and complex normed space over C, and let C⊆X. The set C is absorbing if, for every x∈X, there is t>0 such that x∈tC. It is balanced if λC⊆C for every λ∈K with ∣λ∣≤1. It is absolutely convex if it is both convex and balanced. No closedness, openness, or positive definiteness is part of these definitions.

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

Minkowski functional of an absorbing set

Definition

For an absorbing subset C of a normed space X, its Minkowski functional or gauge is

pC(x):=inf⁡{t>0:x∈tC}(x∈X).

The defining set is nonempty by absorption, so pC(x) is finite and nonnegative. It is not asserted to be a norm or a seminorm: those conclusions need additional hypotheses on C.

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

The gauge of a convex absorbing set is sublinear

Statement

If C⊆X is convex and absorbing, then its gauge satisfies pC(rx)=rpC(x) for r≥0 and pC(x+y)≤pC(x)+pC(y). Thus pC is a real sublinear functional.

Facts & Assumptions

Given: A convex absorbing set C⊆X and x,y∈X.

[F1]

The gauge is pC(z)=inf⁡{t>0:z∈tC}, and its defining set is nonempty (Minkowski functional of an absorbing set).

Proof

technique · direct
1.1F1givenalgebra

For r>0, rx∈tC holds exactly when x∈(t/r)C; taking infima gives pC(rx)=rpC(x), while r=0 gives pC(0)=0.

1.2F1givenchoose

Absorption and convexity first give 0∈C. Given a>pC(x) and b>pC(y), choose s<a, t<b with x∈sC, y∈tC; convexity with 0 enlarges these to x=ac, y=bd for some c,d∈C. Then (ac+bd)/(a+b)∈C, hence x+y∈(a+b)C.

2.1step 1.2F1algebra∎

Therefore pC(x+y)≤a+b for every such a,b; letting them decrease to the two infima proves subadditivity.

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

The gauge of an absolutely convex absorbing set is a seminorm

Statement

If C is absolutely convex and absorbing, then pC(λx)=∣λ∣pC(x) for every scalar λ, and pC is a seminorm. It need not be positive definite.

Facts & Assumptions

Given: An absolutely convex absorbing C⊆X, x∈X, and λ∈K.

[F1]

For convex absorbing C, pC is nonnegative, subadditive, and homogeneous for nonnegative real scalars (The gauge of a convex absorbing set is sublinear).

Proof

technique · direct
1.1F1givenalgebra

If λ=0 the assertion follows from [F1]. For λ≠0, balancedness gives (λ/∣λ∣)C=C: one inclusion is balancedness and the reverse follows by applying it to the inverse scalar.

2.1step 1.1F1algebra∎

Hence λx∈tC exactly when x∈(t/∣λ∣)C, so taking infima yields pC(λx)=∣λ∣pC(x). Together with [F1] this is precisely the seminorm axioms.

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

An open convex neighbourhood is recovered from its gauge

Statement

If U⊆X is open, convex, and 0∈U, then U is absorbing and

U={x∈X:pU(x)<1}.

Facts & Assumptions

Given: An open convex U⊆X containing 0.

[F1]

The gauge is defined for absorbing sets by an infimum over positive dilates (Minkowski functional of an absorbing set).

Proof

technique · direct
1.1givenF1choose

Openness gives B(0,r)⊆U for some r>0. For any x, x∈(∥x∥/r+1)U, so U is absorbing and [F1] applies.

2.1step 1.1F1given

If x∈U, openness gives ε>0 with (1+ε)x∈U; hence pU(x)≤(1+ε)−1<1.

3.1step 1.1F1choose∎

If pU(x)<1, choose t<1 with x∈tU, say x=tu. Convexity and 0∈U imply tu∈U. Thus both inclusions hold.

DefinitionDefinition: Literature-sourcedProof: Not applicableOpen item page →

Weak, strict, and strong separation

Definition

For nonempty A,B⊆X, a nonzero f∈X∗ weakly separates A and B if sup⁡a∈ARe⁡f(a)≤inf⁡b∈BRe⁡f(b). It strictly separates them if Re⁡f(a)<Re⁡f(b) for every a∈A,b∈B, and strongly separates them if there are α<β with Re⁡f(a)≤α<β≤Re⁡f(b) for all a,b. Over R, Re⁡f=f; over C these real parts are essential, since complex values are not ordered.

TheoremStatement: Literature-sourcedProof: AI-generatedverified 2026-09-23 (gpt-6-sol)Open item page →

Separate a point from an open convex set

Statement

Assume the Axiom of Choice. Let U be a nonempty open convex subset of a real or complex normed space X and let x0∉U. Then a nonzero f∈X∗ satisfies

Re⁡f(u)<Re⁡f(x0)(u∈U).

Facts & Assumptions

Given: The Axiom of Choice, a nonempty open convex U and x0∉U.

[F1]

If an open convex set contains 0, it equals the strict unit sublevel set of its gauge (An open convex neighbourhood is recovered from its gauge).

[F2]

Assuming the Axiom of Choice, a real linear functional dominated by a sublinear functional on a linear subspace extends to the whole real vector space with the same domination (Hahn-Banach dominated extension theorem for real vector spaces).

[F3]

A real linear functional u on a complex space yields the complex-linear functional u(x)−iu(ix) with real part u (A complex linear functional is recovered from its real part by f(x)=u(x)-iu(ix)).

[F4]

The gauge of a convex absorbing set is a real sublinear functional (The gauge of a convex absorbing set is sublinear).

Proof

technique · direct
1.1givenF1choose

Choose u0∈U and put V=U−u0, y=x0−u0. Then y≠0 and V is open, convex, contains 0, and y∉V; by [F1], pV(y)≥1 and pV(v)<1 for v∈V.

2.1step 1.1F1F2F4construct

By [F1], V is absorbing, and [F4] makes pV sublinear. On the real line Ry define g(ty)=t. For t≥0, g(ty)=t≤tpV(y)=pV(ty); for t<0, g(ty)<0≤pV(ty). Thus [F2] gives a real linear h on X with h≤pV and h(y)=1.

3.1step 2.1F3given

Choose r>0 with B(0,r)⊆V. For t>∥z∥/r one has z/t∈V and −z/t∈V, so taking infima gives pV(±z)≤∥z∥/r. Domination applied to both z and −z gives ∣h(z)∣≤∥z∥/r. In the real case take f=h; in the complex case take f(z)=h(z)−ih(iz), which is continuous by this estimate and has real part h by [F3].

4.1step 1.1step 2.1step 3.1F1algebra∎

For u=u0+v∈U, [F1] and h≤pV give Re⁡f(u)−Re⁡f(u0)=h(v)<1=h(y)=Re⁡f(x0)−Re⁡f(u0). Since h(y)=1, f is nonzero. Hence the stated strict separation holds.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-09-23 (gpt-6-sol)Open item page →

Separation of disjoint convex sets when one is open

Statement

Assume the Axiom of Choice. If U,V⊆X are nonempty disjoint convex sets and U is open, then there is a nonzero f∈X∗ such that

Re⁡f(u)<Re⁡f(v)(u∈U,v∈V).

Facts & Assumptions

Given: The Axiom of Choice and nonempty disjoint convex sets U,V, with U open.

[F1]

An exterior point and a nonempty open convex set admit a strict separating continuous functional (Separate a point from an open convex set).

[A1]

The Axiom of Choice is used through the Hahn–Banach extension in [F1].

Proof

technique · direct
1.1givenalgebra

The difference D=U−V is open and convex, and 0∉D because U∩V=∅.

2.1step 1.1F1A1

Under [A1], apply [F1] to D and 0. It supplies nonzero f∈X∗ with Re⁡f(d)<0 for every d∈D.

3.1step 2.1algebra∎

For u∈U and v∈V, u−v∈D, so Re⁡f(u)−Re⁡f(v)<0. This is the required strict separation.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-09-23 (gpt-6-sol)Open item page →

Strong separation of a closed and a compact convex set

Statement

Assume the Axiom of Choice. Let C,K⊆X be disjoint nonempty convex sets, where C is closed and K is compact. Then they are strongly separated by a nonzero functional in X∗.

Facts & Assumptions

Given: The Axiom of Choice and disjoint nonempty convex C,K, with C closed and K compact.

[F2]

A continuous real-valued function on a compact metric space attains its minimum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F3]

Disjoint convex sets, one open, are strictly separated by a nonzero continuous functional (Separation of disjoint convex sets when one is open).

[A1]

The Axiom of Choice supplies the Hahn–Banach premise in [F3].

Proof

technique · direct
1.1F1F2givenchoose

By [F1]--[F2], d(k,C) has a minimum δ on K. It is positive: a zero minimum would put some k∈K in the closed set C. Choose 0<r<δ.

2.1step 1.1F3A1

The thickening W=C+B(0,r) is open and convex and is disjoint from K. Under [A1], apply [F3] to W,K to obtain nonzero f with Re⁡f(w)<Re⁡f(k) for w∈W,k∈K.

3.1step 2.1algebra∎

For c∈C, take the supremum over b∈B(0,r) in the inequalities from step 2.1. Since sup⁡∥b∥<rRe⁡f(b)=r∥f∥, this gives Re⁡f(c)+r∥f∥≤Re⁡f(k) for every k∈K. Hence sup⁡CRe⁡f+r∥f∥≤inf⁡KRe⁡f, a positive gap.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-09-23 (gpt-6-sol)Open item page →

A closed convex set is an intersection of closed half-spaces

Statement

Assume the Axiom of Choice. Every nonempty closed convex C⊆X is the intersection of the closed affine half-spaces that contain C.

Facts & Assumptions

Given: The Axiom of Choice and a nonempty closed convex set C⊆X.

[F1]

Disjoint convex sets with one open are strictly separated by a nonzero continuous functional (Separation of disjoint convex sets when one is open).

Proof

technique · direct
1.1given

Since every closed affine half-space in the family contains C, their intersection contains C.

1.2givenF1choose

If x∉C, choose r>0 with B(x,r)∩C=∅. The set C+B(0,r/2) is open and convex and still omits x; [F1], using AC through its open-convex point-separation supplier, gives a nonzero continuous f with Re⁡f(c+b)<Re⁡f(x) for every c∈C and ∥b∥<r/2.

2.1step 1.2algebra∎

Taking the supremum over ∥b∥<r/2 in step 1.2 gives Re⁡f(c)+(r/2)∥f∥≤Re⁡f(x) for every c∈C. Since f≠0, the closed half-space Hx={z:Re⁡f(z)≤Re⁡f(x)−(r/4)∥f∥} contains C and excludes x. Thus every exterior point is excluded from the intersection, proving equality.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-06Open item page →

Continuous annihilator of a linear subspace

Definition

Let X be a normed space and let M⊆X be a linear subspace. Its continuous annihilator is

M⊥:={f∈X∗:f(m)=0 for every m∈M}.

This is an annihilator in the topological dual X∗, not in the unrestricted algebraic dual.

TheoremStatement: Literature-sourcedProof: AI-generatedverified 2026-09-24 (gpt-6-sol)Open item page →

Geometric Hahn--Banach theorem for subspaces

Statement

Assume the Axiom of Choice. For a linear subspace M⊆X and x∉M‾, there is f∈M⊥ with f(x)=1.

Facts & Assumptions

Given: The Axiom of Choice, A subspace M⊆X and x∉M‾.

[A1]

AC is used through norm-preserving extension [F2] in step 3.1.

[F2]

A bounded functional on any subspace extends to the ambient normed space without increasing its norm (A bounded linear functional on an arbitrary subspace extends with the same norm, without assuming the subspace is closed).

Proof

technique · direct
1.1F1givenconstruct

By [F1], δ=dist⁡(x,M)>0. On M+Kx define g(m+λx)=λ; the representation is unique because x∉M.

2.1step 1.1F1algebra

For λ≠0, ∥m+λx∥=∣λ∣∥x+m/λ∥≥∣λ∣δ, while the case λ=0 is immediate. Thus ∥g∥≤1/δ.

3.1step 2.1F2∎

Extend g by [F2] to f∈X∗. Then f∣M=0 and f(x)=1, so f∈M⊥ as required.

CorollaryStatement: Literature-sourcedProof: AI-generatedverified 2026-09-24 (gpt-6-sol)Open item page →

The annihilator detects the closure of a subspace

Statement

Assume the Axiom of Choice. For every linear subspace M⊆X,

M‾=⋂f∈M⊥ker⁡f.

Facts & Assumptions

Given: The Axiom of Choice, A linear subspace M⊆X.

[A1]

AC is used through geometric Hahn–Banach [F1] in step 1.2.

[F1]

Every point outside M‾ is sent to 1 by some continuous functional vanishing on M (Geometric Hahn--Banach theorem for subspaces).

Proof

technique · direct
1.1given

If z∈M‾ and f∈M⊥, continuity of f and f∣M=0 give f(z)=0. Thus M‾ lies in the intersection.

1.2F1given

If z∉M‾, [F1] gives f∈M⊥ with f(z)=1, so z is absent from the intersection.

2.1step 1.1step 1.2∎

The two inclusions prove the formula.

CorollaryStatement: Literature-sourcedProof: AI-generatedverified 2026-09-24 (gpt-6-sol)Open item page →

Density is characterized by a zero annihilator

Statement

Assume the Axiom of Choice. A linear subspace M⊆X is dense if and only if M⊥={0}.

Facts & Assumptions

Given: The Axiom of Choice, A linear subspace M⊆X.

[A1]

AC is used through annihilator closure [F1] in step 2.1.

[F1]

M‾=⋂f∈M⊥ker⁡f (The annihilator detects the closure of a subspace).

Proof

technique · direct
1.1F1given

If M is dense, [F1] says every f∈M⊥ vanishes on X, hence is zero.

2.1F1given∎

If M⊥={0}, the intersection in [F1] is X, so M‾=X and M is dense.

CorollaryStatement: Literature-sourcedProof: AI-generatedverified 2026-09-24 (gpt-6-sol)Open item page →

Finite-dimensional subspaces are complemented

Statement

Assume the Axiom of Choice. Every finite-dimensional linear subspace M of a normed space X is complemented in X.

Facts & Assumptions

Given: The Axiom of Choice, A finite-dimensional subspace M⊆X.

[A1]

AC is used through functional extension [F2] in step 1.1.

[F1]

Relative to a fixed finite basis, every coordinate functional on a finite-dimensional normed space is bounded (A chosen algebraic basis identifies a finite-dimensional normed space with a coordinate space).

[F2]

A bounded functional on a subspace extends norm-preservingly to the ambient normed space (A bounded linear functional on an arbitrary subspace extends with the same norm, without assuming the subspace is closed).

[F3]

A subspace is complemented exactly when it is the range of a bounded projection (A closed subspace is complemented exactly when it is the range of a bounded projection).

Proof

technique · direct
1.1givenF1F2choose

Choose a basis e1,…,en of M, and let ϕj:M→K be its coordinate maps. By [F1]--[F2], extend each ϕj to fj∈X∗.

2.1step 1.1algebra

Define P:X→X by P(x)=∑j=1nfj(x)ej. It is bounded, has range in M, and for m=∑ajej∈M satisfies P(m)=m.

3.1step 2.1F3∎

Thus P2=P and ran⁡P=M; [F3] makes M complemented.

CorollaryStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06Open item page →

Closed finite-codimensional subspaces are complemented

Statement

Every closed finite-codimensional linear subspace M of a normed space X is complemented in X.

Facts & Assumptions

Given: A closed subspace M⊆X with finite-dimensional X/M.

[F1]

The quotient seminorm is a norm exactly when the subspace is closed (The quotient seminorm is a norm exactly when the subspace is closed).

[F2]

Coordinate functionals for a fixed basis of a finite-dimensional normed space are bounded (A chosen algebraic basis identifies a finite-dimensional normed space with a coordinate space).

Proof

technique · direct
1.1F1F2givenchoose

By [F1], Q=X/M is a normed finite-dimensional quotient. Choose a basis q1,…,qn of Q, representatives xj∈X, and bounded coordinate maps ϕj supplied by [F2].

2.1step 1.1algebra

The map S:Q→X, S(q)=∑jϕj(q)xj, is bounded and satisfies πS=IQ. Hence P=IX−Sπ is bounded, P2=P, and ran⁡P=M.

3.1step 2.1F3∎

By [F3], M is complemented.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-09-06Open item page →

Linear hyperplane

Definition

Let X be a vector space over a field F. A linear hyperplane of X is a linear subspace H such that X/H is finite-dimensional over F and dim⁡F(X/H)=1. This is algebraic codimension one; closedness is an additional topological property, not part of the definition.

TheoremStatement: Literature-sourcedProof: AI-generatedverified 2026-09-24 (gpt-6-sol)Open item page →

Closed hyperplanes are kernels of nonzero functionals

Statement

A linear hyperplane H⊆X is closed if and only if H=ker⁡f for some nonzero f∈X∗.

Facts & Assumptions

Given: A linear hyperplane H⊆X.

[F1]

Since a linear hyperplane has codimension one, for any x0∉H each x∈X has a unique decomposition x=h+tx0 with h∈H and t∈K (Linear hyperplane).

[F2]

Proof

technique · direct
1.1givenF1chooseconstruct

Suppose H is closed and choose x0∉H. By [F1], define f(h+tx0):=t on X. Uniqueness of the decomposition makes f well defined and linear, with f(x0)=1 and ker⁡f=H.

2.1F1F2step 1.1algebra

By [F2], δ=dist⁡(x0,H)>0. For x=h+tx0 with t≠0, the vector x/t=x0+h/t has norm at least δ, since −h/t∈H. Hence ∣f(x)∣=∣t∣≤δ−1∥x∥; the same bound is clear for t=0. Thus f is bounded and nonzero, so f∈X∗ and H=ker⁡f.

3.1givenalgebra∎

Conversely, if H=ker⁡f with f∈X∗ nonzero, continuity makes H closed. The induced nonzero map X/H→K is injective and onto, so dim⁡(X/H)=1.

TheoremStatement: Literature-sourcedProof: AI-generatedverified 2026-09-23 (gpt-6-sol)Open item page →

Mazur theorem: weak and norm closure agree for convex sets

Statement

Assume the Axiom of Choice. For a convex subset C of a normed space X, its norm closure equals its weak closure. Here the weak topology is generated by the basic neighbourhoods of x

{y:∣fj(y−x)∣<ε (1≤j≤n)}

for finitely many fj∈X∗ and some ε>0.

Facts & Assumptions

Given: The Axiom of Choice, a convex set C⊆X, and D=C‾∥⋅∥.

[F1]

Disjoint convex sets, one open, are strictly separated by a nonzero continuous functional (Separation of disjoint convex sets when one is open).

[A1]

The Axiom of Choice is used through the Hahn–Banach extension behind [F1].

Proof

technique · direct
1.1given

Every f∈X∗ is norm-continuous, so every displayed basic weak neighbourhood is norm-open. Thus every weak-open set is norm-open, and D⊆C‾weak.

1.2givenF1A1choose

If C=∅, both closures are empty. Otherwise D is nonempty; if x∉D, choose r>0 with x∉D+B(0,r). This latter set is open and convex, so under [A1], [F1] yields f≠0 with Re⁡f(d+b)<Re⁡f(x) for d∈D, ∥b∥<r.

2.1step 1.2algebra

Taking suprema over b∈B(0,r) gives sup⁡d∈DRe⁡f(d)+r∥f∥≤Re⁡f(x). The weak neighbourhood {y:∣f(y−x)∣<r∥f∥/2} therefore misses D, hence misses C.

3.1step 1.1step 2.1∎

Thus x is not in the weak closure whenever it is not in D, proving the reverse inclusion and equality.

DefinitionDefinition: Literature-sourcedProof: Not applicableverified 2026-09-09 (codex)Open item page →

The sequence spaces c_0 and ell-infinity

Definition

Let K=R or C, with absolute value in the real case and modulus ∣a+ib∣=a2+b2 in the complex case. A scalar sequence here is a function x:N→K, including index zero. Let

ℓ∞={x=(xn)n∈N:there is C≥0 with ∣xn∣≤C for all n},c0={x∈ℓ∞:xn→0},

both equipped with ∥x∥∞=sup⁡n∈N∣xn∣. Thus c0 is a specified linear subspace of the bounded-sequence space ℓ∞.

For each bounded sequence, the nonempty real set {∣xn∣:n∈N} has a finite supremum by The Cauchy-sequence reals have the least-upper-bound property. This proves that the displayed norm exists, rather than presuming existence in the definition of boundedness. Its uniqueness requires no choice of supremum witnesses.

Here xn→0 means that for every real ε>0 there is N∈N such that ∣xn∣<ε for all n≥N. Addition and scalar multiplication are coordinatewise. The scalar triangle inequality makes bounded sequences and null sequences linear spaces and gives the triangle inequality for the displayed supremum norm. Absolute homogeneity follows coordinatewise, and a zero supremum forces every coordinate to vanish.

LemmaStatement: Literature-sourcedProof: AI-generatedaudited 2026-09-06Open item page →

c_0 is a closed subspace of ell-infinity

Statement

c0 is a closed linear subspace of ℓ∞ in the sup norm.

Facts & Assumptions

Given: The sequence spaces c0⊆ℓ∞.

[F1]

c0 consists of bounded sequences tending to zero, with the sup norm (The sequence spaces c_0 and ell-infinity).

Proof

technique · direct
1.1F1given

Sums and scalar multiples of null sequences are null, so c0 is a linear subspace.

1.2F1givenchoose

If x(j)∈c0 and ∥x(j)−x∥∞→0, choose j with this norm below ε/2, then N with ∣xn(j)∣<ε/2 for n≥N. Thus ∣xn∣<ε for n≥N.

2.1step 1.2∎

Hence x∈c0 and the subspace is closed.

5 · Examples, counterexamples and false statements

None yet.

Sources