Proposition 2.2 (complete-lattice clause)

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.commutant_complete_closure

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

prove2quantum

In a complete orthomodular lattice the commutant is closed under arbitrary ambient joins and meets. Thus its inherited order is complete; the empty join and meet 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

/-- Proposition 2.2; de Groote, Observables I, PDF pp. 22.
Restored in moderation: source background status is not a formalization obstacle. -/
theorem commutant_complete_closure {L : Type u} [CompleteLattice L]
    (perp : L → L) (horth : IsOrthomodular perp) (S : Set L) :
    ∀ t : Set L, t ⊆ latticeCommutant perp S →
      sSup t ∈ latticeCommutant perp S ∧ sInf t ∈ latticeCommutant perp S := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

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

Read-back

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

Let $L$ be any complete lattice and let $\perp:L\to L$ satisfy, for every $x,y\in L$ ,

x\wedge\perp x=\bot,\qquad x\vee\perp x=\top,\qquad \perp(x\wedge y)=\perp x\vee\perp y,\qquad \perp(x\vee y)=\perp x\wedge\perp y,\qquad \perp(\perp x)=x,

and suppose that $x\wedge(y\vee z)=(x\wedge y)\vee(x\wedge z)$ whenever $y\le x$ and $z\le\perp x$ . For any subset $S\subseteq L$ , put

C=\{b\in L:\ \forall a\in S,\ a=(a\wedge b)\vee(a\wedge\perp b)\}.

Then for every subset $t\subseteq L$ with $t\subseteq C$ , both $\bigvee t$ and $\bigwedge t$ belong to $C$ . This includes $t=\varnothing$ , whose supremum and infimum are $\bot$ and $\top$ , respectively, and includes $S=\varnothing$ , for which $C=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