Proposition 3.20

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.hilbert_quasipoint_finite_dimension_dichotomy

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

prove2quantum

For a quasipoint $\mathfrak B$ in the closed-subspace lattice of a complex Hilbert space, containing a finite-dimensional subspace is equivalent to being generated by a unique line $V$ :

\mathfrak B=\{U:V\subseteq U\},\qquad\dim V=1.

Containing no finite-dimensional subspace is equivalent to containing every subspace of finite codimension. Lines are intrinsic subspaces, independent of a choice of nonzero vector.

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.20; de Groote, Observables I, PDF p./pp. 65.
-/
theorem hilbert_quasipoint_finite_dimension_dichotomy {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (B : StoneSpectrum (ClosedSubmodule ℂ H)) :
    ((∃ U : ClosedSubmodule ℂ H, U ∈ B.val ∧ FiniteDimensional ℂ U.toSubmodule) ↔
      ∃! V : ClosedSubmodule ℂ H, Module.rank ℂ V = 1 ∧ B.val = principalQuasipoint V) ∧
    ((¬ ∃ U : ClosedSubmodule ℂ H, U ∈ B.val ∧ FiniteDimensional ℂ U.toSubmodule) ↔
      ∀ W : ClosedSubmodule ℂ H, FiniteDimensional ℂ W.orthogonal.toSubmodule → W ∈ B.val) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

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

Read-back

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

Let $H$ be a complete complex inner product space, and let $B$ be a quasipoint of its closed complex-linear subspaces: $B$ is a nonempty family excluding the zero subspace, every pair of its members contains a common member of $B$ , and it is maximal under inclusion among families with these properties. Both of the following equivalences hold. First, $B$ contains a finite-dimensional closed subspace if and only if there exists exactly one closed subspace $V$ whose complex dimension, expressed as module rank, is $1$ and for which

B=\{W\subseteq H:W\text{ is a closed complex-linear subspace and }V\subseteq W\}.

Any finite-dimensional member witnessing the left side is necessarily nonzero because $B$ excludes zero. Second, $B$ contains no finite-dimensional closed subspace if and only if every closed subspace $W$ whose orthogonal complement $W^\perp$ is finite-dimensional belongs to $B$ . This quantification includes $W=0$ whenever $H$ is finite-dimensional.

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