Prove2Me

rem-2.1 (complete-lattice clause)

Proved
QAlgorithms.Papers.Independent.Intakethird100.P20.orthocomplement_complete_demorgan

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

prove2quantum

If the ortholattice is complete, orthocomplement interchanges arbitrary meets and joins, including empty families: (⋀s)⊥=⋁a∈sa⊥(\bigwedge s)^\perp=\bigvee_{a\in s}a^\perp and (⋁s)⊥=⋀a∈sa⊥(\bigvee s)^\perp=\bigwedge_{a\in s}a^\perp.

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-2.1; de Groote, Observables I, PDF pp. 20.
Restored in moderation: source background status is not a formalization obstacle. -/
theorem orthocomplement_complete_demorgan {L : Type u} [CompleteLattice L]
    (perp : L → L) (hperp : IsOrthocomplement perp) :
    ∀ s : Set L, perp (sInf s) = sSup (perp '' s) ∧
      perp (sSup s) = sInf (perp '' s) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end
Source
Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 20, rem-2.1
Read-back

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

Let LL be any complete lattice and let ⊥:L→L\perp:L\to L satisfy, for all 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 for every subset s⊆Ls\subseteq L,

⊥ ⁣(⋀s)=⋁{⊥x:x∈s},⊥ ⁣(⋁s)=⋀{⊥x:x∈s}.\perp\!\left(\bigwedge s\right)=\bigvee\{\perp x:x\in s\}, \qquad \perp\!\left(\bigvee s\right)=\bigwedge\{\perp x:x\in s\}.

The subset ss may be empty; in that case these identities assert ⊥⊤=⊥\perp\top=\bot and ⊥⊥=⊤\perp\bot=\top, respectively.

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