Prove2Me

Proposition 2.1

Open
QAlgorithms.Papers.Independent.Intakethird100.P20.commutation_symmetric_iff_orthomodular

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

prove2quantum

For a bounded lattice with the designated orthocomplement, the relation aCb  ⟺  a=(a∧b)∨(a∧b⊥)aCb\iff a=(a\wedge b)\vee(a\wedge b^\perp) is symmetric if and only if the lattice is orthomodular. Completeness is not assumed.

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.1; de Groote, Observables I, PDF pp. 21.
Restored in moderation: source background status is not a formalization obstacle. -/
theorem commutation_symmetric_iff_orthomodular {L : Type u} [Lattice L] [BoundedOrder L]
    (perp : L → L) (hperp : IsOrthocomplement perp) :
    (∀ a b : L, LatticeCommutes perp a b → LatticeCommutes perp b a) ↔
      IsOrthomodular perp := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end
Source
Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 21, Proposition 2.1
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.

Then the assertion that, for every a,b∈La,b\in L,

a=(a∧b)∨(a∧⊥b)⟹b=(b∧a)∨(b∧⊥a)a=(a\wedge b)\vee(a\wedge\perp b) \quad\Longrightarrow\quad b=(b\wedge a)\vee(b\wedge\perp a)

is equivalent to the conjunction of the five displayed identities with the following additional condition: for every a,b,c∈La,b,c\in L such that b≤ab\le a and c≤⊥ac\le\perp a,

a∧(b∨c)=(a∧b)∨(a∧c).a\wedge(b\vee c)=(a\wedge b)\vee(a\wedge c).
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