Prove2Me

Proposition 3.24

Open
QAlgorithms.Papers.Independent.Intakethird100.P20.sector_quasipoints_are_boolean_quasipoints

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

prove2quantum

For a Boolean sector SS of a complete orthomodular lattice, the proper ultrafilters of the Boolean algebra SS are exactly the Boolean quasipoints of the ambient lattice contained in SS:

Q(S)={β∈Qb(L):β⊆S},Q(S)=\{\beta\in Q^b(L):\beta\subseteq S\},

where subsets of SS are identified with their images in LL. Sectors use the proof-intended sub-ortholattice convention. No topology on all Boolean quasipoints is introduced.

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

/-- Proposition 3.24; de Groote, Observables I, PDF p./pp. 69.
Source convention: Boolean sectors are maximal distributive sub-ortholattices; generation includes complements and bounds.
-/
theorem sector_quasipoints_are_boolean_quasipoints {L : Type u} [CompleteLattice L] (perp : L → L) (horth : IsOrthomodular perp)
    (S : Set L) (hS : IsBooleanSector perp S) :
    letI : Bot S := ⟨⟨⊥, hS.1.1⟩⟩
    ∀ B : Set S, IsQuasipoint B ↔ IsBooleanQuasipoint perp (Subtype.val '' B) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end
Source
Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 69, Proposition 3.24
Read-back

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

Let LL be any complete lattice, and let a↦a⊥a\mapsto a^\perp be a function on LL satisfying, for all a,b∈La,b\in L,

a∧a⊥=⊥,a∨a⊥=⊤,(a∧b)⊥=a⊥∨b⊥,(a∨b)⊥=a⊥∧b⊥,(a⊥)⊥=a,a\wedge a^\perp=\bot,\qquad a\vee a^\perp=\top,\qquad (a\wedge b)^\perp=a^\perp\vee b^\perp,\qquad (a\vee b)^\perp=a^\perp\wedge b^\perp,\qquad (a^\perp)^\perp=a,

and, for all a,b,c∈La,b,c\in L with b≤ab\le a and c≤a⊥c\le a^\perp,

a∧(b∨c)=(a∧b)∨(a∧c).a\wedge(b\vee c)=(a\wedge b)\vee(a\wedge c).

Let S⊆LS\subseteq L contain ⊥,⊤\bot,\top, be closed under a↦a⊥a\mapsto a^\perp, binary meets, and binary joins, and satisfy both distributive identities

a∧(b∨c)=(a∧b)∨(a∧c),a∨(b∧c)=(a∨b)∧(a∨c)a\wedge(b\vee c)=(a\wedge b)\vee(a\wedge c),\qquad a\vee(b\wedge c)=(a\vee b)\wedge(a\vee c)

for all a,b,c∈Sa,b,c\in S. Assume also that every T⊆LT\subseteq L containing SS and having these same closure and distributivity properties equals SS. Give SS its inherited order and bottom element ⊥\bot. Then, for every family B⊆SB\subseteq S, the following are equivalent: BB is nonempty, excludes ⊥\bot, has for every a,b∈Ba,b\in B some c∈Bc\in B with c≤a,bc\le a,b, and is maximal under inclusion among families in SS with these three properties; and its underlying image A={a∈L:a is the underlying element of some member of B}A=\{a\in L:a\text{ is the underlying element of some member of }B\} is nonempty, excludes ⊥\bot, has for every a,b∈Aa,b\in A some c∈Ac\in A with c≤a,bc\le a,b, satisfies

a=(a∧b)∨(a∧b⊥)for every a,b∈A,a=(a\wedge b)\vee(a\wedge b^\perp)\qquad\text{for every }a,b\in A,

and is maximal under inclusion among all subsets of LL satisfying these four properties. The maximality on the latter side ranges over subsets of all of LL. Empty BB is included in the quantification and satisfies neither side.

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