Lemma 2.1

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.commutant_antitone_double_triple

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

prove2quantum

For subsets $S,T$ of an orthomodular lattice, $S\subseteq T$ implies $T^C\subseteq S^C$ , every $S$ is contained in $S^{CC}$ , and $S^C=S^{CCC}$ . Both empty and nonempty subsets use the same commutant formula.

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

/-- Lemma 2.1; de Groote, Observables I, PDF pp. 23.
Restored in moderation: source background status is not a formalization obstacle. -/
theorem commutant_antitone_double_triple {L : Type u} [Lattice L] [BoundedOrder L]
    (perp : L → L) (horth : IsOrthomodular perp) (S T : Set L) :
    (S ⊆ T → latticeCommutant perp T ⊆ latticeCommutant perp S) ∧
    S ⊆ latticeCommutant perp (latticeCommutant perp S) ∧
    latticeCommutant perp S =
      latticeCommutant perp (latticeCommutant perp (latticeCommutant perp S)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 23, Lemma 2.1

Read-back

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

Let $L$ be any bounded 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 each subset $A\subseteq L$ , define

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

Then for every pair of subsets $S,T\subseteq L$ , all three assertions hold: if $S\subseteq T$ , then $C(T)\subseteq C(S)$ ; one has $S\subseteq C(C(S))$ ; and $C(S)=C(C(C(S)))$ . The subsets $S$ and $T$ may be empty, and $C(\varnothing)=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