Existence of orthogonal representations (supporting Lemma 3.6)

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.orthogonal_representation_exists

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

prove2quantum

For an abelian concrete von Neumann algebra, every element in the complex linear span of its nonzero projections admits a finite sum of pairwise orthogonal nonzero projections with complex coefficients. Zero coefficients are allowed. The zero element admits the empty representation.

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

/-- orthogonal-representation-existence; de Groote, Observables I, PDF pp. 59, 60.
Restored in moderation: source background status is not a formalization obstacle. -/
theorem orthogonal_representation_exists {H : Type u} [NormedAddCommGroup H]
    [InnerProductSpace ℂ H] [CompleteSpace H] (R : VonNeumannAlgebra H)
    (hcomm : ∀ a b : R.toStarSubalgebra, a * b = b * a) (x : R.toStarSubalgebra)
    (hx : x ∈ Submodule.span ℂ {a : R.toStarSubalgebra |
      ∃ p : Projection R, p.val ≠ 0 ∧ (a : H →L[ℂ] H) = p.val}) :
    ∃ (n : ℕ) (c : Fin n → ℂ) (p : Fin n → Projection R),
      IsOrthogonalRepresentation x c p := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 60, Unnumbered construction preceding Lemma 3.6

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 $R$ be a von Neumann algebra of bounded complex-linear operators on $H$ . Assume that $ab=ba$ for every $a,b\in R$ . For every $x\in R$ lying in the complex linear span of the nonzero projections in $R$ , where a projection is a self-adjoint idempotent operator, there exist a natural number $n\ge 0$ , complex coefficients $c_0,\ldots,c_{n-1}$ , and projections $p_0,\ldots,p_{n-1}\in R$ such that every $p_i$ is nonzero, $p_i p_j=0$ whenever $i\ne j$ , and $x=\sum_{i=0}^{n-1}c_i p_i$ . The coefficients may be zero and need not be distinct. The case $n=0$ is allowed: the projection conditions are then vacuous and the empty sum equals zero.

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