Proposition 3.26

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.orthonormal_basis_unique_boolean_sector

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

prove2quantum

Let $(e_k)_{k\in K}$ be an orthonormal basis of an arbitrary complex Hilbert space. There is a unique Boolean sector containing all basis lines, and it is the actual subset

S=\{U\in L(H):\forall k,\ e_k\in U\text{ or }e_k\in U^\perp\}.

Every line $\mathbb C e_k$ belongs to this sector. Sectors are maximal distributive sub-ortholattices. The zero-space, empty-basis case is retained.

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.26; de Groote, Observables I, PDF p./pp. 72.
Source convention: Boolean sectors are maximal distributive sub-ortholattices; generation includes complements and bounds.
-/
theorem orthonormal_basis_unique_boolean_sector {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    {K : Type v} (e : HilbertBasis K ℂ H) :
    let S : Set (ClosedSubmodule ℂ H) := {U | ∀ k, e k ∈ U ∨ e k ∈ U.orthogonal}
    IsBooleanSector (fun U : ClosedSubmodule ℂ H => U.orthogonal) S ∧
    (∀ k, closedLine (e k) ∈ S) ∧
    ∀ T : Set (ClosedSubmodule ℂ H),
      IsBooleanSector (fun U : ClosedSubmodule ℂ H => U.orthogonal) T →
      (∀ k, closedLine (e k) ∈ T) → T = S := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 72, Proposition 3.26

Read-back

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

Let $H$ be a complete complex inner product space, let $K$ be any index type, and let $(e_k)_{k\in K}$ be a Hilbert basis of $H$ , meaning an orthonormal family with dense linear span. Define the family of closed complex linear subspaces

S=\{U\subseteq H:U\text{ is a closed complex linear subspace and, for every }k\in K,\ e_k\in U\text{ or }e_k\in U^\perp\}.

For families of closed subspaces, consider the following properties: containing $\{0\}$ and $H$ ; closure under orthogonal complements, binary intersections, and binary joins, where $U\vee V=\overline{U+V}$ ; and satisfaction, for every three members $U,V,W$ , of both identities

U\cap(V\vee W)=(U\cap V)\vee(U\cap W),\qquad U\vee(V\cap W)=(U\vee V)\cap(U\vee W).

Then $S$ has all these properties and is maximal under inclusion among families having them. Moreover, for every $k\in K$ , $S$ contains the closed subspace

\ell_k=\bigcap\{U:U\text{ is a closed complex linear subspace of }H,\ e_k\in U\},

and every family $T$ of closed complex linear subspaces that has the stated properties, is maximal among families having them, and contains every $\ell_k$ , equals $S$ . No finiteness or countability condition is imposed on $K$ ; the empty index type is included, in which case the Hilbert basis assumption forces $H=\{0\}$ , and all conditions quantified over $k$ are vacuous.

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