boolean-filter-upward-extension

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.boolean_quasipoint_upward_extension

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

prove2quantum

Let $\beta$ be a Boolean quasipoint in an orthomodular lattice. If $c$ commutes with every member of $\beta$ and lies above some member, then

c\in\beta.

The commutation requirement is retained; ordinary upward closure is not asserted for a Boolean quasipoint in the whole ambient lattice.

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

/-- boolean-filter-upward-extension; de Groote, Observables I, PDF p./pp. 69.
-/
theorem boolean_quasipoint_upward_extension {L : Type u} [Lattice L] [BoundedOrder L] (perp : L → L)
    (horth : IsOrthomodular perp) (B : Set L) (hB : IsBooleanQuasipoint perp B)
    (c : L) (hcomm : ∀ a ∈ B, LatticeCommutes perp a c)
    (habove : ∃ b ∈ B, b ≤ c) : c ∈ B := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 69, boolean-filter-upward-extension

Read-back

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

Let $L$ be a bounded lattice, and let $a\mapsto a^\perp$ be a function on $L$ satisfying $a\wedge a^\perp=\bot$ , $a\vee a^\perp=\top$ , $(a\wedge b)^\perp=a^\perp\vee b^\perp$ , $(a\vee b)^\perp=a^\perp\wedge b^\perp$ , and $(a^\perp)^\perp=a$ for all $a,b\in L$ , as well as

b\leq a,\quad d\leq a^\perp \quad\Longrightarrow\quad a\wedge(b\vee d)=(a\wedge b)\vee(a\wedge d)

for all $a,b,d\in L$ . Let $B\subseteq L$ be nonempty, exclude $\bot$ , have for every $a,b\in B$ some $d\in B$ with $d\leq a$ and $d\leq b$ , and satisfy $a=(a\wedge b)\vee(a\wedge b^\perp)$ for every $a,b\in B$ . Assume $B$ is maximal under inclusion among subsets with all these properties. If $c\in L$ satisfies $a=(a\wedge c)\vee(a\wedge c^\perp)$ for every $a\in B$ , and there exists $b\in B$ with $b\leq c$ , then $c\in B$ .

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