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.

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 Analytic Hahn Banach Theorem - Examples

1 · Prerequisites

2 · Summary

The companion page keeps the analytic theorem concrete. It compares the abstract norming-functional existence theorem with the explicit LpLq extremizer, computes a full interval of norm-preserving extensions in a codimension-one example, and then uses the dominated form of Hahn-Banach to build a Banach limit and verify its standard properties.

The counterexample isolates nonuniqueness as a reusable phenomenon, while the closing remark records two open choice-theoretic questions that the proved Hahn-Banach ledger does not settle.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

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

The abstract norming-functional theorem agrees with the concrete L^p-L^q formula

Example

Let (X,A,μ) be a measure space, let 1p<, and let q be conjugate to p. Assume either 1<p<, or p=1 and μ is sigma-finite. For every nonzero fLp(μ), the abstract Hahn-Banach theorem produces a unit-norm functional Φ(Lp(μ)) with Φ(f)=fp, and the earlier LpLq duality page realizes the same value concretely by pairing against the usual Lq extremizer.

Facts & Assumptions

Given: A measure space (X,A,μ), an exponent 1p< with conjugate exponent q, and a nonzero element fLp(μ) in one of the ranges covered by the LpLq duality page.

[L1]

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

[L2]

In the same LpLq ranges, the Lp norm is the supremum of pairings against unit Lq functions (The Lp norm is the supremum of pairings against unit Lq functions).

Verification

technique · direct
1.1

Apply [L1] to the nonzero vector fLp(μ). This gives a functional Φ(Lp(μ)) with Φ=1 and Φ(f)=fp.

L1given
1.2

By [L2], the same number fp is obtained as sup{fgdμ:gq1}. In the standard explicit realization, one takes g=fp1sgnf/fpp1 when 1<p<, and g=sgnf when p=1.

L2givenalgebra
2.1

Thus the abstract existence statement from Hahn-Banach and the concrete LpLq formula from the earlier page identify the same norming phenomenon: one proves that some unit functional attains fp, and the other writes an attaining functional down explicitly.

step 1.1step 1.2
ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

A codimension-one subspace can admit many norm-preserving Hahn-Banach extensions

Example

Let X=(R2,), let M:=span{(1,1)}, and define f0:MR by f0(t,t)=t. Then f0=1, and for every c[1,1] the formula

Fc(a,b):=1+c2a+1c2b

defines a norm-preserving extension of f0 to all of X. So a codimension-one subspace can have infinitely many Hahn-Banach extensions of the same norm.

Facts & Assumptions

Given: The normed space X=(R2,), the diagonal subspace M=span{(1,1)}, and the functional f0(t,t)=t.

[L1]

In a one-step Hahn-Banach extension, the admissible values form a nonempty interval (The admissible values in a one-step Hahn-Banach extension form a nonempty interval).

[L2]

Verification

technique · direct
1.1

For (t,t)M one has f0(t,t)=t=(t,t), so f0=1. Also every (a,b)R2 decomposes as (a,b)=a+b2(1,1)+ab2(1,1), so X=MR(1,1).

givenalgebra
2.1

If F is a linear extension of f0 and c:=F(1,1), then step 1.1 forces F(a,b)=a+b2F(1,1)+ab2F(1,1)=1+c2a+1c2b. Conversely, the displayed formula defines a linear functional extending f0.

step 1.1givenconstructalgebra
3.1

Let φ(a,b):=αa+βb on (R2,). If (a,b)1, then φ(a,b)αa+βbα+β. Choosing a=sgnα and b=sgnβ (interpreting sgn0=0) gives (a,b)1 and φ(a,b)=α+β, so φ=α+β. Applying this to the formula from step 2.1 yields Fc=1+c+1c2. This equals 1 exactly when 1c1.

step 2.1algebra
4.1

Therefore every c[1,1] gives a norm-preserving extension of f0. This computes explicitly the admissible interval predicted abstractly by [L1], and in particular is consistent with the existence statement of [L2].

L1L2step 3.1
ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

A Banach limit obtained from Hahn-Banach

Example

Let be the real vector space of bounded real sequences with the supremum norm, let S: be the shift S(x0,x1,x2,)=(x1,x2,x3,), and let C be the subspace of sequences whose Cesaro means converge.

Then there exists a linear functional L:R such that

  • L(x)=limnσn(x) for every xC;
  • L(x)lim supnσn(x) for every bounded sequence x;
  • L(Sx)=L(x) for every bounded sequence x.

The next lemma shows that such an L is a Banach limit.

Facts & Assumptions

Given: The real vector space of bounded real sequences, the shift S, and the Cesaro means σn(x) of a bounded sequence x.

[L1]

A sublinear functional is additive up to inequality and homogeneous for nonnegative real scalars (A sublinear functional on a real vector space).

[L2]

Dominated real linear functionals extend to the whole ambient real vector space (Hahn-Banach dominated extension theorem for real vector spaces).

[L3]

The nth Cesaro mean is σn(x)=1n+1k=0nxk (The Cesaro means σn=(x0++xn)/(n+1) and (C,1)-summability).

[L6]

A real sequence is a function on N, so bounded sequences are a special class of sequences in the sense of Sequences of reals: bounded, eventually, frequently, tails, subsequences.

Verification

technique · direct
1.1

Define p:R by p(x):=lim supnσn(x). If x, choose M0 with xnM for all n; then every Cesaro mean satisfies σn(x)M, so [L4] shows that p(x) is an ordinary real number. Because σn(x+y)=σn(x)+σn(y) for every n, [L5] gives p(x+y)p(x)+p(y). Also σn(tx)=tσn(x) for every t0, so p(tx)=tp(x). Thus p is sublinear in the sense of [L1].

L1L3L4L5L6givenconstructalgebra
2.1

Let C be the set of sequences whose Cesaro means converge, and define λ(x):=limnσn(x)(xC). Since σn(ax+by)=aσn(x)+bσn(y) for all real scalars a,b, the set C is a linear subspace and λ is linear. If xC, then the convergent sequence (σn(x)) has limit superior equal to its limit, so λ(x)p(x). Therefore [L2] yields a linear extension L:R of λ with Lp on all of .

L2L3L4step 1.1givenconstructalgebra
3.1

Let x=(xn). Since x is bounded, there is M0 with xnM for all n. Using [L3], σn(xSx)=1n+1k=0n(xkxk+1)=x0xn+1n+1. Hence σn(xSx)x0+Mn+10, so xSxC and λ(xSx)=0. Since L extends λ, L(xSx)=0, that is, L(Sx)=L(x).

L3step 2.1givenalgebra
4.1

Step 2.1 gives the extension and domination properties, and step 3.1 gives shift invariance. Therefore L has all three properties listed in the example.

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

A Banach limit is positive, has norm one, is shift invariant, and lies between liminf and limsup

Statement

Let L:R be a functional as in A Banach limit obtained from Hahn-Banach. Then:

  1. L is positive: if xn0 for all n, then L(x)0.
  2. L is shift invariant.
  3. L=1 for the supremum norm on .
  4. For every bounded real sequence x, lim infnxnL(x)lim supnxn.

So L is a Banach limit.

Facts & Assumptions

Given: A bounded real sequence x, its limit inferior and limit superior, and a functional L:R with the three properties constructed in A Banach limit obtained from Hahn-Banach.

[L1]

The previous example gives a linear functional L extending Cesaro limit, dominated by lim supσn, and shift invariant (A Banach limit obtained from Hahn-Banach).

[L2]

For a real sequence, lim infxn and lim supxn are defined from tail infima and tail suprema (Limit superior and limit inferior of a real sequence as infnsupknxk and supninfknxk in R).

[L3]

The Cesaro means of a constant sequence are equal to that constant (The Cesaro means σn=(x0++xn)/(n+1) and (C,1)-summability).

Proof

technique · direct
1.1

Shift invariance is part of [L1]. Let 1=(1,1,1,). By [L3], every Cesaro mean of 1 equals 1, so the extension property in [L1] gives L(1)=1. By linearity, L(c1)=c(cR).

L1L3givenalgebra
1.2

Suppose xn0 for every n. Then every Cesaro mean of x is nonpositive, so lim supnσn(x)0. The domination part of [L1] therefore gives L(x)=L(x)lim supnσn(x)0, hence L(x)0. So L is positive.

L1L4givenalgebra
2.1

Let M:=x. Then M1xM1 termwise, so the sequences M1x and M1+x are pointwise nonnegative. By step 1.2, 0L(M1x)=ML(x)and0L(M1+x)=M+L(x). Thus L(x)M=x, so L1. Since step 1.1 gives L(1)=1 and 1=1, one also has L1. Therefore L=1.

step 1.1step 1.2givenalgebra
2.2

Write α:=lim infnxn and β:=lim supnxn. Let ε>0. By the definition in [L2], there is NN such that for all kN, αεxkβ+ε. Hence every term of the shifted sequence SNx lies between the constant sequences (αε)1 and (β+ε)1. Using positivity from step 1.2, the constant-sequence values from step 1.1, and shift invariance from [L1], we get αε=L((αε)1)L(SNx)=L(x)L((β+ε)1)=β+ε.

L1L2step 1.1step 1.2givenchoosealgebra
3.1

Since the inequalities of step 2.2 hold for every ε>0, one obtains αL(x)β. Together with steps 1.1, 1.2, and 2.1, this shows that L is a Banach limit.

step 2.2
CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

Hahn-Banach norm-preserving extensions need not be unique

Statement refuted

For a bounded linear functional on a subspace of a normed space, a norm-preserving Hahn-Banach extension to the whole space is unique.

Facts & Assumptions

Given: The diagonal subspace M=span{(1,1)}(R2,) and the functional f0(t,t)=t on M.

[L1]

For every c[1,1], the functional Fc(a,b)=1+c2a+1c2b is a norm-preserving extension of f0 (A codimension-one subspace can admit many norm-preserving Hahn-Banach extensions).

Counterexample

technique · direct
1.1

By [L1], the functionals F1(a,b)=aandF1(a,b)=b are both norm-preserving extensions of f0.

L1given
2.1

They agree on M, since F1(t,t)=t=F1(t,t) for every (t,t)M, but they differ on (1,1): F1(1,1)=11=F1(1,1).

step 1.1givenalgebra
3.1

Thus the same functional on the same subspace has two distinct norm-preserving Hahn-Banach extensions. Therefore the uniqueness claim is false.

step 1.1step 2.1
RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-05 rests on unproved materialOpen item page →
Rests on 2 statements 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.

Two choice-theoretic consequences of Hahn-Banach remain open

Remark

The established choice ledger for Hahn-Banach is summarized in The set-theoretic cost of Hahn-Banach. Two natural next questions are still not settled in ZF:

This page does not use either implication. They are recorded here only as local signposts, so that the reader does not mistake the proved choice-strength consequences for a complete classification.

Sources