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.

Stone duality for a power set algebra

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $B = P (N)$ be the power-set Boolean algebra of a discrete countable set. Then the Stone space (ultrafilter space) of $B$ is the Stone–Čech compactification $β N$ of $N$ (The Stone–Čech compactification by its compact-Hausdorff extension property): its points are the ultrafilters on $N$ , the principal ultrafilters form a dense copy of $N$ , the basic clopens are $[A] = {U : A \in U}$ for $A \subseteq N$ , and the map $A \mapsto [A]$ is the canonical isomorphism $P (N) ≅ Clop (β N)$ of Stone representation for Boolean algebras.

Facts & Assumptions

Given: The Axiom of Choice, the Boolean algebra $P (N)$ , its ultrafilter space with basic clopens $[A]$ , and the discrete space $N$ .

[L1]

The map $A \mapsto [A]$ is a Boolean isomorphism $P (N) ≅ Clop (Ult (P (N)))$ and the ultrafilter space is compact Hausdorff with a clopen basis, so it is a Stone space (Stone representation for Boolean algebras, The Axiom of Choice).

[L2]

Every proper filter on $N$ extends to an ultrafilter, and an ultrafilter contains exactly one of $A$ , $N ∖ A$ ; the principal ultrafilters are the $U_{n} = {A : n \in A}$ (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter, Boolean algebra and Boolean ultrafilter, The Axiom of Choice).

[L3]

Under the ultrafilter lemma every ultrafilter on a compact Hausdorff space converges to a unique point, and a topological space is compact exactly when every ultrafilter on it converges (Assuming the ultrafilter lemma, compactness is equivalent to every net having a cluster point, every net having a convergent subnet, every filter having a cluster point, and every ultrafilter converging, The Axiom of Choice).

[L4]

A Stone–Čech compactification of $X$ is a Hausdorff compactification $(B, i)$ such that every continuous map from $X$ into a compact Hausdorff space extends uniquely (The Stone–Čech compactification by its compact-Hausdorff extension property).

[L5]

A compact Hausdorff space is regular: if $p$ belongs to an open set $V$ , there is an open $W ∋ p$ with $\overline{W} \subseteq V$ (A compact Hausdorff space is regular and normal, hence $T_{3}$ and $T_{4}$ ).

Verification

technique · direct

1.1

The ultrafilters on $P (N)$ are exactly the maximal filters of subsets of $N$ ("set ultrafilters") by the complement dichotomy [L2]; the principal ultrafilters $U_{n}$ are pairwise distinct and ${U_{n}} = [{n}]$ is open, so the map $n \mapsto U_{n}$ is an injective continuous map from discrete $N$ onto a discrete subspace.

L1L2algebra

1.2

The image ${U_{n} : n \in N}$ is dense in the ultrafilter space: a nonempty basic clopen $[A]$ with $A \neq \emptyset$ contains $U_{n}$ for every $n \in A$ .

1.1L1algebra

1.3

Let $K$ be compact Hausdorff and $f : N \to K$ continuous (that is, arbitrary). For an ultrafilter $U$ on $N$ let $f_{*} U : = {B \subseteq K : f^{- 1} (B) \in U}$ , an ultrafilter on $K$ , which converges to a unique point by [L3]; define $F (U)$ to be that limit.

L3algebra

1.4

The map $F$ extends $f$ : for the principal ultrafilter $U_{n}$ the pushforward $f_{*} U_{n}$ is the principal ultrafilter at $f (n)$ , which converges to $f (n)$ , so $F (U_{n}) = f (n)$ .

1.3L2algebra

2.1

The map $F$ is continuous. Let $F (U) \in V$ with $V \subseteq K$ open. By [L5] choose an open $W$ with $F (U) \in W$ and $\overline{W} \subseteq V$ . Since $f_{*} U$ converges to $F (U)$ , one has $W \in f_{*} U$ , equivalently $f^{- 1} (W) \in U$ , so the basic open $[f^{- 1} (W)]$ contains $U$ . If $U^{'}$ lies in this basic open, then $W \in f_{*} U^{'}$ ; because $f_{*} U^{'}$ converges to $F (U^{'})$ , its limit lies in $\overline{W}$ (otherwise the open complement of $\overline{W}$ would also belong to the ultrafilter). Thus $F (U^{'}) \in \overline{W} \subseteq V$ , proving $[f^{- 1} (W)] \subseteq F^{- 1} (V)$ and hence continuity.

step 1.3L1L3L5algebra

2.2

Uniqueness: $F$ is determined on the dense subset ${U_{n} : n \in N}$ by [step 1.2] and [step 1.4], and $K$ is Hausdorff, so two continuous extensions agree.

step 1.1step 1.2step 1.4algebra

3.1

By [step 1.1], [step 1.2], [step 2.1] and [step 2.2] the pair (ultrafilter space, $n \mapsto U_{n}$ ) is a Hausdorff compactification of $N$ satisfying the universal property [L4], so it is a Stone–Čech compactification; by [L1] the basic clopens are the $[A]$ and the algebra of clopens is canonically $P (N)$ .

step 1.1step 1.2step 2.1step 2.2L1L4∎

Remarks

The example is the identity case of Stone duality: the Stone space of $P (N)$ is $β N$ , whose Algebra of clopens is again $P (N)$ .
No new choice is used beyond the ultrafilter lemma, which is the declared form of the Axiom of Choice in this run.

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

Marcus Tressl, Stone Duality for Boolean Algebras — Example 2.3.2, p. 8; the beta-N universal-property verification is local from the declared Stone–Čech suppliers (standard reference, not scraped)