Theorem 3.2

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.gelfand_stone_canonical_homeomorphism

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

prove2quantum

Let $\mathcal A$ be a unital abelian von Neumann algebra on an arbitrary complex Hilbert space. Its Gelfand spectrum, consisting of nonzero continuous multiplicative linear functionals with the weak dual topology, is canonically homeomorphic to its projection-lattice Stone spectrum:

\Omega(\mathcal A)\xrightarrow{\ \cong\ }Q(\mathcal A),\qquad \tau\longmapsto\{P\in P(\mathcal A):\tau(P)=1\}.

For a quasipoint $\mathfrak B$ , the inverse character takes value $1$ on its projections and $0$ on the others. On finite spectral sums its value is $\sum_j c_j\mathbf1_{\mathfrak B}(P_j)$ ; it is a continuous character on the entire algebra. No normality of characters, finite dimensionality or separability is asserted.

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

/-- Theorem 3.2; de Groote, Observables I, PDF p./pp. 61, 62.
-/
theorem gelfand_stone_canonical_homeomorphism {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (R : VonNeumannAlgebra H)
    (hcomm : ∀ a b : R.toStarSubalgebra, a * b = b * a) :
    ∃ h : WeakDual.characterSpace ℂ R.toStarSubalgebra ≃ₜ StoneSpectrum (Projection R),
      (∀ chi, (h chi).val = {p | chi ⟨p.val, p.prop.1⟩ = 1}) ∧
      (∀ B (p : Projection R), (h.symm B) ⟨p.val, p.prop.1⟩ =
        @ite ℂ (p ∈ B.val) (Classical.propDecidable _) 1 0) ∧
      (∀ B (n : ℕ) (c : Fin n → ℂ) (p : Fin n → Projection R),
        (h.symm B) (∑ i, c i • (⟨(p i).val, (p i).prop.1⟩ : R.toStarSubalgebra)) = spectralSumFunction c p B) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 61, Theorem 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, and let $R$ be a von Neumann algebra of bounded complex-linear operators on $H$ , satisfying $ab=ba$ for all $a,b\in R$ . There exists a homeomorphism $h$ from the space of nonzero continuous multiplicative complex-linear functionals on $R$ , with its weak dual topology, onto the quasipoints of the projections of $R$ . A projection here is a self-adjoint idempotent in $R$ ; a quasipoint is a nonempty family of projections excluding zero, every pair of whose members has a common lower bound in the family, maximal under inclusion among such families. Its topology is generated by the sets of quasipoints containing a specified projection. For every character $\chi$ , the underlying family of $h(\chi)$ is exactly $\{p:\chi(p)=1\}$ . For every projection quasipoint $B$ and every projection $p\in R$ ,

h^{-1}(B)(p)= \begin{cases} 1,&p\in B,\\ 0,&p\notin B. \end{cases}

Moreover, for every such $B$ , every natural number $n$ , every family of complex coefficients $c_0,\ldots,c_{n-1}$ , and every family of projections $p_0,\ldots,p_{n-1}\in R$ ,

h^{-1}(B)\!\left(\sum_{i=0}^{n-1}c_i p_i\right) =\sum_{\substack{0\leq i<n\\p_i\in B}}c_i.

This last assertion imposes no nonzero or orthogonality conditions on the projections and includes $n=0$ , when both sums are 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