Corollary 3.4

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.open_lattice_stone_compact

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

prove2quantum

For every topological space $M$ , the Stone spectrum of its lattice of open sets is compact:

Q(T(M))\text{ is compact}.

No Hausdorff, compactness or nonemptiness assumption is imposed on $M$ itself.

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

/-- Corollary 3.4; de Groote, Observables I, PDF p./pp. 56.
-/
theorem open_lattice_stone_compact {M : Type u} [TopologicalSpace M] : CompactSpace (StoneSpectrum (Opens M)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 56, Corollary 3.4

Read-back

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

For every topological space $M$ , form the set $\mathcal Q(\mathcal O(M))$ of inclusion-maximal nonempty families $B$ of open subsets of $M$ that exclude $\varnothing$ and such that any two members contain a common member of $B$ . Equip this set with the topology generated by $\{B:U\in B\}$ as $U$ ranges over the open subsets of $M$ . Then $\mathcal Q(\mathcal O(M))$ is compact. There are no separation, compactness, local compactness, or nonemptiness assumptions on $M$ ; in particular, the assertion includes $M=\varnothing$ , whose quasipoint space 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