rem-2.2

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.commutant_finite_join_distribution

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

prove2quantum

Every element $a$ of $S$ distributes over the join of a finite family in $S^C$ : $a\wedge\bigvee b=\bigvee(a\wedge b)$ . The empty family gives $a\wedge0=0$ . Arbitrary families in a complete lattice are covered by the supporting statement.

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_finite_join_distribution {L : Type u} [Lattice L] [BoundedOrder L]
    (perp : L → L) (horth : IsOrthomodular perp) (S : Set L) (a : L) (ha : a ∈ S)
    {n : ℕ} (b : Fin n → L) (hb : ∀ i, b i ∈ latticeCommutant perp S) :
    a ⊓ Finset.univ.sup b = Finset.univ.sup (fun i => a ⊓ b i) := 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 bounded 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$ , let $n$ be any natural number, and let $(b_i)_{i=0}^{n-1}$ be any family in $L$ such that, for every index $i$ and every $s\in S$ ,

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

Then

a\wedge\bigvee_{i=0}^{n-1}b_i =\bigvee_{i=0}^{n-1}(a\wedge b_i).

The value $n=0$ is included: the condition on the family is then vacuous, both joins are $\bot$ , 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