stone-boolean-representation

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.stone_boolean_representation

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

prove2quantum

For every Boolean algebra, its quasipoint spectrum with the membership topology is compact, zero dimensional and Hausdorff. The map $a\mapsto Q_a$ is an order isomorphism onto its clopen Boolean algebra, hence a Boolean-algebra isomorphism. The trivial Boolean algebra and empty spectrum are included.

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

/-- stone-boolean-representation; de Groote, Observables I, PDF pp. 8, 39.
Restored in moderation: source background status is not a formalization obstacle. -/
theorem stone_boolean_representation {L : Type u} [BooleanAlgebra L] :
    CompactSpace (StoneSpectrum L) ∧ T2Space (StoneSpectrum L) ∧
    TopologicalSpace.IsTopologicalBasis {s : Set (StoneSpectrum L) | IsClopen s} ∧
    ∃ e : L ≃o Clopens (StoneSpectrum L),
      ∀ a : L, (e a : Set (StoneSpectrum L)) = stoneBasic a := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 8, stone-boolean-representation

Read-back

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

For any Boolean algebra $L$ , let $X$ be the set of all subsets $B\subseteq L$ that are nonempty, exclude $\bot$ , satisfy that for every $a,b\in B$ there exists $c\in B$ with $c\le a$ and $c\le b$ , and are maximal under inclusion among subsets satisfying these three conditions. Equip $X$ with the topology generated by the sets $U_a=\{B\in X:a\in B\}$ for $a\in L$ . Then $X$ is compact and Hausdorff, the collection of all subsets of $X$ that are both open and closed is a topological basis, and there exists an order isomorphism $e$ from $L$ to the clopen subsets of $X$ , ordered by inclusion, such that the underlying subset of $e(a)$ is exactly $U_a$ for every $a\in L$ . The Boolean algebra may have $\bot=\top$ ; in that case $X$ is empty.

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