rem-2.2 (complete-lattice clause)

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.commutant_arbitrary_join_distribution

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

prove2quantum

For a complete orthomodular lattice, every $a\in S$ distributes over every join from $S^C$ , including empty families: $a\wedge\bigvee t=\bigvee_{b\in t}(a\wedge b)$ .

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.2; de Groote, Observables I, PDF pp. 23.
Restored in moderation: source background status is not a formalization obstacle. -/
theorem commutant_arbitrary_join_distribution {L : Type u} [CompleteLattice L]
    (perp : L → L) (horth : IsOrthomodular perp) (S : Set L) (a : L) (ha : a ∈ S)
    (t : Set L) (ht : t ⊆ latticeCommutant perp S) :
    a ⊓ sSup t = sSup ((fun b => a ⊓ b) '' t) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

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

Read-back

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

Let $L$ be any complete 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$ . Let $S\subseteq L$ , let $a\in L$ satisfy $a\in S$ , and let $t\subseteq L$ satisfy that for every $b\in t$ and every $s\in S$ ,

s=(s\wedge b)\vee(s\wedge\perp b).

Then

a\wedge\bigvee t=\bigvee\{a\wedge b:b\in t\}.

The set $t$ may be empty, in which case its hypothesis is vacuous and the equality reads $a\wedge\bot=\bot$ . The hypothesis $a\in S$ requires $S$ to be nonempty.

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