Proposition 3.7

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.frame_stone_extremally_disconnected

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

prove2quantum

Let $L$ be a complete lattice satisfying the frame law $a\wedge\bigvee S=\bigvee_{b\in S}(a\wedge b)$ . Then its Stone spectrum is extremally disconnected, and

\overline{\bigcup_{a\in S}Q_a(L)}=Q_{\bigvee S}(L)\qquad(S\subseteq L).

Thus the closure of every open subset of the spectrum is open. The frame law is the source's meaning of complete distributivity, not the stronger modern two-index law.

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

/-- Proposition 3.7; de Groote, Observables I, PDF p./pp. 45.
-/
theorem frame_stone_extremally_disconnected {L : Type u} [CompleteLattice L] (hframe : HasFrameLaw L) :
    ExtremallyDisconnected (StoneSpectrum L) ∧
      ∀ s : Set L, closure (⋃ a ∈ s, stoneBasic a) = stoneBasic (sSup s) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 45, Proposition 3.7

Read-back

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

Let $L$ be a complete lattice satisfying $a\wedge\sup s=\sup\{a\wedge b:b\in s\}$ for every $a\in L$ and every subset $s\subseteq L$ , including the empty subset. Let $\mathcal Q(L)$ consist of the inclusion-maximal nonempty subsets $B\subseteq L$ excluding $\bot$ such that any two members have a common lower bound in $B$ , and give it the topology generated by $D(a)=\{B\in\mathcal Q(L):a\in B\}$ . Then $\mathcal Q(L)$ is extremally disconnected, meaning the closure of every open subset is open, and for every subset $s\subseteq L$ ,

\overline{\bigcup_{a\in s}D(a)}=D(\sup s).

This includes $s=\varnothing$ , for which $\sup s=\bot$ and both sides are 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