example-3.2

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.cofinite_subspaces_quasidistributive_not_distributive

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

prove2quantum

For an infinite-dimensional complex Hilbert space, let $L_{\mathrm{cof}}(H)$ consist of zero and all closed subspaces of finite codimension. It is closed under the inherited binary meet and join, is not distributive, and has exactly one quasipoint:

Q(L_{\mathrm{cof}}(H))=\{L_{\mathrm{cof}}(H)\setminus\{0\}\}.

Consequently the basic sets satisfy the quasidistributive identity $Q_{(U\wedge V)\vee(U\wedge W)}=Q_{U\wedge(V\vee W)}$ . This is the concrete counterexample separating quasidistributivity from distributivity.

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

/-- example-3.2; de Groote, Observables I, PDF p./pp. 43.
-/
theorem cofinite_subspaces_quasidistributive_not_distributive {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (hinfinite : ¬ FiniteDimensional ℂ H) :
    (∀ U V : CofiniteSubspaces H,
      ((U.val ⊓ V.val = ⊥ ∨ FiniteDimensional ℂ (U.val ⊓ V.val).orthogonal.toSubmodule) ∧
       (U.val ⊔ V.val = ⊥ ∨ FiniteDimensional ℂ (U.val ⊔ V.val).orthogonal.toSubmodule))) ∧
    (∃ U V W : CofiniteSubspaces H,
      U.val ⊓ (V.val ⊔ W.val) ≠ (U.val ⊓ V.val) ⊔ (U.val ⊓ W.val)) ∧
    IsQuasipoint {U : CofiniteSubspaces H | U.val ≠ ⊥} ∧
    (∀ B : StoneSpectrum (CofiniteSubspaces H), B.val = {U | U.val ≠ ⊥}) ∧
    (∀ U V W : CofiniteSubspaces H,
      cofiniteBasic ((U.val ⊓ V.val) ⊔ (U.val ⊓ W.val)) =
        cofiniteBasic (U.val ⊓ (V.val ⊔ W.val))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 43, example-3.2

Read-back

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

Let $H$ be a complete complex inner product space that is not finite-dimensional over $\mathbb C$ . Let $\mathcal C(H)$ consist of the closed complex linear subspaces $U\subseteq H$ such that either $U=\{0\}$ or $U^\perp$ is finite-dimensional, ordered by inclusion, with bottom element $\{0\}$ . Here meets and joins of underlying closed subspaces mean intersection and closed linear span, respectively. A quasipoint of $\mathcal C(H)$ means an inclusion-maximal nonempty family $B\subseteq\mathcal C(H)$ excluding $\{0\}$ such that any two members have a common lower bound belonging to $B$ . For any closed subspace $X$ , define $D(X)$ to be the set of these quasipoints $B$ for which some member of $B$ has underlying subspace $X$ . Then all of the following hold: for every $U,V\in\mathcal C(H)$ , each of $U\wedge V$ and $U\vee V$ is either $\{0\}$ or has finite-dimensional orthogonal complement; there exist $U,V,W\in\mathcal C(H)$ with $U\wedge(V\vee W)\ne(U\wedge V)\vee(U\wedge W)$ ; the family $\{U\in\mathcal C(H):U\ne\{0\}\}$ is a quasipoint; every quasipoint of $\mathcal C(H)$ equals that family; and, for every $U,V,W\in\mathcal C(H)$ , $D((U\wedge V)\vee(U\wedge W))=D(U\wedge(V\vee W))$ .

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