stone-topology-properties

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.stone_topology_properties

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

prove2quantum

For a bounded lattice $L$ , the membership sets form a clopen basis for $Q(L)$ and satisfy

Q_{a\wedge b}=Q_a\cap Q_b,\qquad Q_0=\varnothing,\qquad Q_1=Q(L).

The Stone spectrum is Hausdorff, zero-dimensional and completely regular. No compactness is asserted for an arbitrary lattice.

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-topology-properties; de Groote, Observables I, PDF p./pp. 40.
-/
theorem stone_topology_properties {L : Type u} [Lattice L] [BoundedOrder L] :
    (∀ a b : L, stoneBasic (a ⊓ b) = stoneBasic a ∩ stoneBasic b) ∧
    stoneBasic (⊥ : L) = ∅ ∧ stoneBasic (⊤ : L) = Set.univ ∧
    (∀ a : L, IsClopen (stoneBasic a)) ∧
    TopologicalSpace.IsTopologicalBasis (Set.range (stoneBasic : L → Set (StoneSpectrum L))) ∧
    TopologicalSpace.IsTopologicalBasis {s : Set (StoneSpectrum L) | IsClopen s} ∧
    T2Space (StoneSpectrum L) ∧ CompletelyRegularSpace (StoneSpectrum L) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 40, stone-topology-properties

Read-back

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

Let $L$ be any bounded lattice. Let $\mathcal Q(L)$ be the set of all inclusion-maximal subsets $B\subseteq L$ that are nonempty, exclude $\bot$ , and contain, for each $a,b\in B$ , some $c\le a,b$ . For $a\in L$ , put $D(a)=\{B\in\mathcal Q(L):a\in B\}$ , and equip $\mathcal Q(L)$ with the topology generated by the sets $D(a)$ . Then $D(a\wedge b)=D(a)\cap D(b)$ for all $a,b\in L$ , $D(\bot)=\varnothing$ , and $D(\top)=\mathcal Q(L)$ ; every $D(a)$ is both open and closed; the collection $\{D(a):a\in L\}$ is a topological basis; the collection of all subsets of $\mathcal Q(L)$ that are both open and closed is also a topological basis; and $\mathcal Q(L)$ is Hausdorff and completely regular. No nontriviality assumption on $L$ is imposed; when $\bot=\top$ , $\mathcal Q(L)$ 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