rem-2.1

Proved

QAlgorithms.Papers.Independent.Intakethird100.P20.orthocomplement_bounds_and_order

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

prove2quantum

In any bounded ortholattice the designated orthocomplement exchanges the bounds and reverses order: $0^\perp=1$ , $1^\perp=0$ , and $a\le b\iff b^\perp\le a^\perp$ . The arbitrary-meet/join clause is the supporting statement for complete lattices.

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_bounds_and_order {L : Type u} [Lattice L] [BoundedOrder L]
    (perp : L → L) (hperp : IsOrthocomplement perp) :
    perp ⊥ = ⊤ ∧ perp ⊤ = ⊥ ∧ ∀ a b : L, a ≤ b ↔ perp b ≤ perp a := 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 $L$ be any bounded lattice and let $\perp:L\to L$ be a function satisfying, for all $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.

Then $\perp\bot=\top$ and $\perp\top=\bot$ , and for every $a,b\in L$ one has $a\le b$ if and only if $\perp b\le\perp a$ . The assumptions allow the bounded lattice with $\bot=\top$ .

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