Lemma 3.8

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.stonean_clopens_recover_space

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

For a Stonean space $\Omega$ —compact, Hausdorff and extremally disconnected—the Stone spectrum of its clopen-set Boolean algebra is canonically homeomorphic to $\Omega$ :

Q(OC(\Omega))\xrightarrow{\ \cong\ }\Omega,\qquad \mathfrak B\longmapsto\text{the unique point of }\bigcap_{U\in\mathfrak B}U.

The arbitrary join of clopens in this regime is the closure of their union, while the meet is the interior of their intersection; quasipoints only require their usual inclusion order.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P20

open Set TopologicalSpace

open QAlgorithms.Papers.Independent.Next46.P33 (Projection)

open scoped Topology

universe u v

/-- Lemma 3.8; de Groote, Observables I, PDF p./pp. 72.
-/
theorem stonean_clopens_recover_space {M : Type u} [TopologicalSpace M] [CompactSpace M] [T2Space M]
    [ExtremallyDisconnected M] :
    ∃ h : StoneSpectrum (Clopens M) ≃ₜ M,
      ∀ B, (⋂ U : {U : Clopens M // U ∈ B.val}, (U.val : Set M)) = {h B} := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 72, Lemma 3.8

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $M$ be any compact Hausdorff topological space such that the closure of every open set is open. Consider the space $X$ whose points are families $B$ of clopen subsets of $M$ that are nonempty, exclude $\varnothing$ , contain for every $U,V\in B$ some $W\in B$ with $W\subseteq U\cap V$ , and are maximal under inclusion among families with these properties; equip $X$ with the topology generated by the sets $\{B:U\in B\}$ , one for each clopen $U\subseteq M$ . There exists a homeomorphism $h:X\to M$ such that, for every $B\in X$ ,

\bigcap_{U\in B}U=\{h(B)\}.

The space $M$ is allowed to be empty; in that case $X$ is also empty, and the assertion about each $B$ has no instances.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph