Prove2Me

Proposition 2.2

Open
QAlgorithms.Papers.Independent.Intakethird100.P20.commutant_sublattice

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

prove2quantum

In an orthomodular lattice, the commutant SC={b:aCb for every a∈S}S^C=\{b: aCb\text{ for every }a\in S\} contains both bounds and is closed under the designated complement and finite meets and joins, as established in the source proof. Its complete-lattice clause is stated separately.

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_sublattice {L : Type u} [Lattice L] [BoundedOrder L]
    (perp : L → L) (horth : IsOrthomodular perp) (S : Set L) :
    IsSubOrtholattice perp (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 LL be any bounded lattice and let ⊥:L→L\perp:L\to L satisfy, for every x,y∈Lx,y\in L,

x∧⊥x=⊥,x∨⊥x=⊤,⊥(x∧y)=⊥x∨⊥y,⊥(x∨y)=⊥x∧⊥y,⊥(⊥x)=x,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∧(y∨z)=(x∧y)∨(x∧z)x\wedge(y\vee z)=(x\wedge y)\vee(x\wedge z) whenever y≤xy\le x and z≤⊥xz\le\perp x. For any subset S⊆LS\subseteq L, define

C={b∈L: ∀a∈S, a=(a∧b)∨(a∧⊥b)}.C=\{b\in L:\ \forall a\in S,\ a=(a\wedge b)\vee(a\wedge\perp b)\}.

Then ⊥,⊤∈C\bot,\top\in C; for every b∈Cb\in C, one has ⊥b∈C\perp b\in C; and for every b,c∈Cb,c\in C, both b∧cb\wedge c and b∨cb\vee c belong to CC. The subset SS may be empty, in which case C=LC=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