Alphabeta Math
LemmaStatement: AI-adaptedProof: 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.

Zero set ultrafilters and Stone-Cech points

Statement

Assume the Axiom of Choice (The Axiom of Choice), so that the ultrafilter lemma and Dependent Choice are available. Let X be a Tychonoff space (Completely regular spaces and Tychonoff (T312) spaces) and let (βX,e) be its Stone–Čech compactification as supplied by the evaluation theorem (Under the ultrafilter lemma and dependent choice, the closure of the full evaluation image is the Stone–Čech compactification); identify X with e[X]βX. Then the map

p    Up:={ZZ(X):pZβX}

is a bijection from βX onto the set of z-ultrafilters on X (Zero set filter and zero set ultrafilter).

Facts & Assumptions

Given: The Axiom of Choice, a Tychonoff space X, its Stone–Čech compactification βX with embedding e, and the family Z(X) of zero sets of continuous real functions on X.

[L1]

Z(X) is closed under finite intersections, Z(f)Z(g)=Z(f2+g2), and X=Z(0), =Z(1); z-filters and z-ultrafilters are as defined in Zero set filter and zero set ultrafilter (Completely regular spaces and Tychonoff (T312) spaces for Tychonoffness).

[L2]

βX is a compact Hausdorff space, e:XβX is an embedding with dense image, and every continuous u:X[0,1] has a unique continuous extension uˉ:βX[0,1]; the compactification is realised as the closure of X in a cube, so points of βX are separated by the coordinate functions uˉ (Under the ultrafilter lemma and dependent choice, the closure of the full evaluation image is the Stone–Čech compactification, The Axiom of Choice).

[L3]

A family of closed subsets of a compact space has nonempty intersection whenever every finite subfamily has nonempty intersection: otherwise the complements form an open cover and a finite subcover exhibits a finite subfamily with empty intersection.

[L4]

If Zi=Z(fi) and f~i:=min(1,fi)C(X,[0,1]), then Z(f~i)=Zi. If uC(X,[0,1]) vanishes on Z1Z2, define

ui=uf~if~1+f~2off Z1Z2,ui=0on Z1Z2.

Each ui is continuous: away from the common zero this is a quotient of continuous functions, while at a common zero uiu0. Moreover u1+u2=u, ui is [0,1]-valued, and ui vanishes on Zi. This is the decomposition used in [step 3.1]. [algebra]

Proof

technique · direct
1.1

For pβX define ρp(u):=uˉ(p) for uC(X,[0,1]); then ρp(u)1 and ρp is additive, positively homogeneous, multiplicative and lattice-preserving: for u,vC(X,[0,1]) and real λ,μ0 with λu+μv again [0,1]-valued, ρp(λu+μv)=λρp(u)+μρp(v), ρp(uv)=ρp(u)ρp(v), and ρp(max(u,v))=max(ρp(u),ρp(v)); more generally every polynomial identity with nonnegative coefficients valid on X passes to ρp.

L2algebra
1.2

If (xα) is a net in X with e(xα)p in βX, then ρp(u)=limαu(xα) for every uC(X,[0,1]): this is continuity of uˉ at p together with uˉe=u.

L2algebra
2.1

Characterisation of closure points. For AX one has pe[A]βX if and only if ρp(u)=0 for every uC(X,[0,1]) with uA=0. If pe[A] choose a net aαA with e(aα)p and use [step 1.2]. Conversely, if pe[A] take a basic neighbourhood N={q:q(ui)ρp(ui)<ε, in} of p in the cube with Ne[A]= and put w:=max(0, 1ε2in(uiρp(ui))2)C(X,[0,1]); then ρp(w)=max(0,10)=1 by [step 1.1], while w(a)=0 for every aA, since e(a)N means i(ui(a)ρp(ui))2ε2.

step 1.1step 1.2L2algebra
3.1

For pβX, the family Up is a z-filter: it contains X because e[X] is dense in βX; it omits because ρp(1)=10 and 1 vanishes on ; it is upward closed because ZZ implies e[Z]e[Z]; and it is closed under finite intersections: if Zi=Z(fi) with pe[Zi] for i=1,2, take uC(X,[0,1]) vanishing on Z1Z2 and write u=u1+u2 with u1,u2C(X,[0,1]) vanishing on Z1, respectively Z2, by the construction of [L4]; then ρp(ui)=0 by [step 2.1] and ρp(u)=0 by [step 1.1], so pe[Z1Z2] by [step 2.1] again.

step 1.1step 2.1L1L4
3.2

Injectivity. For uC(X,[0,1]) and real c one has pe[{uc}] whenever c>ρp(u): for a net xα with e(xα)p one has u(xα)ρp(u)<c by [step 1.2], so eventually xα{uc}. Conversely, if c<ρp(u) then pe[{uc}]: with v:=min(1,(uc)+) one has ρp(v)=min(1,ρp(u)c)>0 by [step 1.1] and v vanishes on {uc}, so [step 2.1] applies. Hence ρp(u)=inf{cR:Z((uc)+)Up} depends only on Up, and since the coordinates ρp(u) over uC(X,[0,1]) determine the point p of the cube by [L2], the equality Up=Uq forces p=q.

step 1.1step 1.2step 2.1L2
4.1

For pβX the z-filter Up is maximal. Let WUp be a z-filter and let ZZ(X) with ZW; if ZUp, then pe[Z] and [step 2.1] provides uC(X,[0,1]) vanishing on Z with t:=ρp(u)>0; the zero set Z1:=Z((t/2u)+) is disjoint from Z, because u=0 on Z makes (t/2u)+=t/2 there, and belongs to Up, because for any net xαX with e(xα)p one has u(xα)t>t/2 by [step 1.2], so eventually (t/2u(xα))+=0, that is, xαZ1, whence pe[Z1]; but then Z,Z1W give =ZZ1W, contradicting that W is a z-filter. Hence ZUp, and Up is a z-ultrafilter.

step 1.2step 2.1step 3.1L1algebra
5.1

Surjectivity. Let U be a z-ultrafilter. The family {e[Z]:ZU} consists of closed subsets of the compact space βX and has the finite intersection property, because the intersection of finitely many such closures contains e[Z1Zn] with Z1ZnU nonempty; by [L3] there is p in the intersection, so pe[Z] for every ZU, that is, UUp; both are z-filters and U is maximal, so U=Up by [step 4.1].

step 4.1L1L3
6.1

By [step 4.1] every Up is a z-ultrafilter, by [step 5.1] the map pUp is surjective, and by [step 3.2] it is injective; hence it is a bijection onto the set of z-ultrafilters.

step 3.2step 4.1step 5.1

Remarks

  • The functional ρp is the bridge. It is multiplicative even though a point of the cube is not a multiplicative functional on all of Cb(X) by definition; multiplicativity is obtained from [step 1.2], because all coordinates converge along a single net converging to p.
  • No new choice principle is hidden. The single point selected in [step 5.1] comes from the nonemptiness of one intersection, not from a family of nonempty sets; the extension of functions to βX is inherited from the Stone–Čech universal property, whose assumptions (ultrafilter lemma and Dependent Choice) are declared.

Depends on

Used by

Dependency tree · two levels

34 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