rem-3.1

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.distributive_basic_unions

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

prove2quantum

For a bounded distributive lattice,

Q_a\cup Q_b=Q_{a\vee b}.

For any bounded lattice satisfying this union identity, the further identity $Q_{(a\wedge b)\vee(a\wedge c)}=Q_{a\wedge(b\vee c)}$ holds for every $a,b,c$ . This latter consequence does not by itself imply distributivity without order reflection.

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

/-- rem-3.1; de Groote, Observables I, PDF p./pp. 43.
-/
theorem distributive_basic_unions {L : Type u} [Lattice L] [BoundedOrder L] :
    (IsDistributive (L := L) → ∀ a b : L, stoneBasic a ∪ stoneBasic b = stoneBasic (a ⊔ b)) ∧
    ((∀ a b : L, stoneBasic a ∪ stoneBasic b = stoneBasic (a ⊔ b)) →
      ∀ a b c : L, stoneBasic ((a ⊓ b) ⊔ (a ⊓ c)) = stoneBasic (a ⊓ (b ⊔ c))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 43, rem-3.1

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)$ consist of the inclusion-maximal nonempty subsets $B\subseteq L$ excluding $\bot$ such that for every $x,y\in B$ some $z\in B$ satisfies $z\le x,y$ , and put $D(a)=\{B\in\mathcal Q(L):a\in B\}$ . The theorem asserts both of the following implications. If $L$ satisfies both distributive identities $a\wedge(b\vee c)=(a\wedge b)\vee(a\wedge c)$ and $a\vee(b\wedge c)=(a\vee b)\wedge(a\vee c)$ for every $a,b,c\in L$ , then $D(a)\cup D(b)=D(a\vee b)$ for every $a,b\in L$ . Conversely, if $D(a)\cup D(b)=D(a\vee b)$ for every $a,b\in L$ , then $D((a\wedge b)\vee(a\wedge c))=D(a\wedge(b\vee c))$ for every $a,b,c\in L$ .

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