Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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.

Coordinate partial sums on c_0

Example

Let K=R or C and X=c0(K) with the supremum norm and coordinates indexed by N={0,1,}. Define (ej)i=1 if i=j and 0 otherwise. For N0 put PNx=j=0Nxjej. Then X is Banach, each PN:XX is bounded linear, PNxx for each xX, and PN=1 for every N0. These assertions are choice-free. Under ACω, the sequential uniform boundedness theorem also supplies a qualitative uniform bound.

Facts & Assumptions

Given: The specified field, space, coordinate vectors, and finite truncations.

[F1]

c0 consists of bounded null sequences, with coordinatewise operations and the supremum norm (The sequence spaces c_0 and ell-infinity).

[F2]

Every nonempty bounded-above set of reals has a supremum (The Cauchy-sequence reals have the least-upper-bound property); applying this to negatives also supplies infima of nonempty bounded-below sets.

[F3]

Complex norms use the modulus; norm-metric completeness has the same meaning over either scalar field (Real and complex scalar conventions for normed spaces). Modulus is definite, multiplicative, and subadditive (Conjugation is an involutive real-field automorphism, zz=z2, and modulus is definite, multiplicative, and subadditive).

[F5]

A normed space is Banach if every norm-Cauchy sequence converges in it (Banach space).

[F6]

Finite vector sums start at the zero vector and append one summand at each successor (Linear combination of a finite list, and the span span(S) as the smallest linear subspace containing S).

[F7]

A linear map with a bound TxCx is bounded (A bounded linear operator between normed spaces).

[F8]

The norm of a bounded operator is its unit-ball supremum (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[F9]

Under ACω, a pointwise bounded sequence from a Banach space to a normed space has uniformly bounded operator norms (Sequential uniform boundedness under countable choice).

Verification

1.1

We first prove scalar completeness from the real supremum property. A real Cauchy sequence (am) is bounded: take M with amaM<1 for mM and successively take the larger of aM+1 and each of a0,,aM1. This finite process produces a bound B. Each tail has a unique infimum bN=inf{am:mN} in [B,B], and L=sup{bN:NN} exists. Given η>0, take M with alam<η for l,mM. For fixed mM and every NM, all terms in the N-tail are in [amη,am+η], so its nonempty tail has infimum in that same interval. For N<M, bNbMam+η. Thus amηbMLam+η. Using η=ε/2 proves amL. If two scalar limits differed by d>0, sufficiently late terms within d/3 of both would give d<2d/3 by triangle inequality. Hence the limit is unique.

F2algebra
1.2

Each ej is a null sequence of norm one. Computing each coordinate in the finite sum gives (PNx)i=xi for iN and (PNx)i=0 for i>N: when iN the sole nonzero contribution is xi(ei)i=xi, and otherwise every contribution is zero. This calculation follows directly from appending the summands in the recursive finite sum. Thus PNx is eventually zero and lies in c0. At each coordinate, PN(ax+by)i=a(PNx)i+b(PNy)i, so PN is linear. Also (PNx)ix for all i, hence PNxx and PN is bounded.

F1F6F7givenalgebra
2.1

For z=a+ib, the modulus formula yields a,bza+b: the first inequalities follow from a2,b2a2+b2, and the last from (a+b)2=a2+b2+2aba2+b2, comparing nonnegative squares. Therefore the real and imaginary parts of a complex Cauchy sequence are real Cauchy sequences. Their unique limits a,b from step 1.1 give complex limit a+ib, since the modulus of the difference is bounded by the sum of the two coordinate errors. The scalar triangle inequality again proves uniqueness.

F3step 1.1algebra
2.2

The estimate in step 1.2 bounds the unit-ball image by 1. Since PNe0=e0 and e0=1, this image contains 1 as a norm value. Its supremum is therefore exactly PN=1 for every N0, including the one-coordinate projection P0. Also PN0=0.

F8step 1.2algebra
2.3

The coordinate formula gives PNxx=supj>Nxj. Given ε>0, take J with xj<ε/2 for jJ. For NJ the tail supremum is at most ε/2<ε, proving PNxx. If x already vanishes beyond J, the error is exactly zero for NJ.

F1step 1.2algebra
3.1

Let (x(m)) be any norm-Cauchy sequence in c0. For each fixed j, xj(m)xj(l)x(m)x(l), so the coordinate sequence is scalar Cauchy and has a unique limit xj. Replacement applied on N to the unique pair (j,xj) produces a set of these pairs, the graph of a function x:NK. This uses unique existence, not a choice of witnesses from non-singleton sets.

F1F4step 1.1step 2.1
4.1

If x(m)x(l)<η for m,lM, then for fixed mM and j, the scalar triangle inequality gives xj(m)xjη+xj(l)xj. Since the last term tends to zero, xj(m)xjη; a positive excess would be contradicted by making that term smaller than half the excess. Taking η=1 and one such m gives xjx(m)+1 for every j, so x is bounded. All subsequent suprema are legitimate by the real supremum property. Thus for general η the uniform coordinate bound implies x(m)xη for mM. Taking η=ε/2 proves norm convergence in the bounded-sequence space.

F1F2F3step 3.1algebra
5.1

Given ε>0, take one m with xx(m)<ε/2, and then J with xj(m)<ε/2 for jJ, since x(m)c0. For such j, xjxjxj(m)+xj(m)<ε. Hence xc0, and the arbitrary Cauchy sequence converges in c0. This proves c0 is Banach over both fields. The choices here concern a single given ε; no simultaneous selection is used.

F1F3F5step 4.1algebra
6.1

Under ACω, apply the sequential theorem with domain and codomain c0: step 5.1 proves the domain Banach, step 1.2 supplies bounded linear maps and the pointwise bound Mx=x. Its conclusion is a finite common bound for the PN. Step 2.2 has already computed that bound as 1 without any choice principle, and step 2.3 proves the promised convergence.

F9step 5.1step 1.2step 2.2step 2.3

Remarks

This concrete example is library-generated. The local completeness proof develops the coordinate-limit method in MIT 18.102 notes, Theorem 16 and following c0 exercise, printed pp.5–6; those notes leave the c0 case as an exercise. Neither a general basis theorem nor another examples page supplies a premise here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources