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

C zero of a locally compact space

Example

Assume the Axiom of Choice (The Axiom of Choice), inherited from the unitization and Gelfand representation suppliers used below. Let N={0,1,2,… } be discrete, so that c0(N) is exactly C0(N) (The sequence spaces c_0 and ell-infinity, Compact support, Cc(X), and C0(X)). Then:

  1. the characters of c0(N) are exactly the evaluations evn(a)=an, one for each n∈N, and each occurs exactly once;
  2. c0(N) has no unit;
  3. the net of characteristic functions 1F of finite subsets F⊆N, ordered by inclusion, is an approximate unit of c0(N) consisting of positive contractions.

Facts & Assumptions

Given: The discrete space N, the algebra c0(N) with the supremum norm and pointwise operations, the completeness of that norm, and the coordinate projections δn (the characteristic function of {n}).

[L0]

C0(X) consists of continuous functions whose level sets {x:∣f(x)∣≥ϵ} are compact for every ϵ>0 (Compact support, Cc(X), and C0(X)). On discrete N, compact subsets are finite, since the singleton cover has a finite subcover only for a finite set. Thus a sequence belongs to C0(N) exactly when every positive level set is finite, which is equivalent to convergence to zero: a null sequence has each level set inside a finite initial segment, and conversely a finite level set has a largest index, after which all values have modulus below ϵ.

[L1]

c0 is the space of null sequences with the supremum norm, the norm is complete on it (a ∥⋅∥∞-Cauchy sequence of null sequences has coordinatewise limits, the limit is null because ∣an∣≤∣an−an(k)∣+∣an(k)∣ for large k, and the convergence is uniform), and the finite truncations converge in norm to any element of c0 (The sequence spaces c_0 and ell-infinity, Finite truncations approximate null and summable sequences).

[L2]

Once c0(N) is known to be a nonzero genuinely nonunital commutative C*-algebra, every one of its characters extends to a character of its unitization and hence is continuous with ∣χ(a)∣≤∥a∥ (Characters on a unital Banach algebra are continuous, Character space of the unitization is one-point compactification, The Axiom of Choice).

Verification

technique · direct
1.1L0L1algebra

By [L0], c0(N)=C0(N). This space is a nonzero commutative C*-algebra: completeness is [L1], pointwise multiplication and conjugation preserve null sequences, ∥ab∥∞≤∥a∥∞∥b∥∞, and ∥a∗a∥∞=∥a∥∞2; it has no unit, since a unit e would satisfy eδn=δn for every n, hence e(n)=1 for all n, contradicting e∈c0. This proves claim 2 and licenses [L2].

1.2algebra

Each evn is a character of c0(N): it is complex-linear and multiplicative because evaluation at a point is, and it is nonzero because evn(δn)=1 for the coordinate vector δn∈c0(N).

2.1step 1.1L1L2algebra

If χ is a character then χ(δn)∈{0,1} for every n, because δn2=δn gives χ(δn)2=χ(δn) and C is a field; the values are not all zero, since otherwise χ would vanish on all finite truncations by linearity and hence, by continuity from [L2] (licensed by [step 1.1]) and the density of truncations [L1], on all of c0, contradicting that χ≠0; and for m≠n one has 0=χ(δmδn)=χ(δm)χ(δn), so if χ(δn0)=1 then χ(δm)=0 for all m≠n0.

3.1step 2.1L1L2algebra

For a character χ with χ(δn0)=1 and a∈c0(N) one has χ(a)=∑nanχ(δn)=an0: approximate a by its truncations [L1], use linearity on each truncation, and pass to the limit with continuity of χ from [L2]; the series has at most one nonzero term, because χ(δn)=0 for every n≠n0 by [step 2.1], so the limit is an0χ(δn0)=an0 and no summability of a is needed (a general element of c0 need not be summable).

4.1step 1.2step 3.1algebra

Hence every character is some evaluation, evaluations are characters by [step 1.2], and two evaluations are equal only if the indices agree, since evm(δm)=1≠0=evn(δm) for m≠n; this proves claim 1.

5.1L1algebra∎

Claim 3: each 1F is a positive contraction, since 1F2=1F and ∥1F∥∞≤1, and the family of finite subsets is directed by inclusion; for a∈c0 and ϵ>0 choose N with ∣an∣<ϵ for n>N (possible because a is a null sequence [L1]); then for every finite F⊇{0,…,N} one has ∥1Fa−a∥∞=sup⁡n∉F∣an∣≤sup⁡n>N∣an∣<ϵ.

Remarks

  • This is C0(X) for the simplest noncompact X: the character space is N itself, and the absence of a unit is exactly the noncompactness.
  • The example is the concrete companion of Every commutative C star algebra has an approximate unit; the net there consists of compactly supported functions, which on discrete N are precisely the finitely supported sequences.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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