Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Von Neumann closure, standard vectors and modular analytic tools — Examples

1 · Prerequisites

2 · Summary

The example separates two representations of the same finite matrix algebra. In its defining representation every nonzero vector is cyclic, while a nonzero projection kills each vector, so none is separating. In the Hilbert–Schmidt left representation, a faithful density matrix supplies a unit cyclic-separating vector through its positive square root. The example proves both statements directly and identifies the resulting vector functional with the density-matrix trace functional.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

ExampleConstruction: Literature-sourcedVerification: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Defining and Hilbert–Schmidt representations of M_n

Statement

Assume the Axiom of Choice. Let $n > 1$ , let $H = C^{n}$ with its standard inner product linear in the first argument, and let $M = B (H) = M_{n} (C)$ act on $H$ in its defining representation. Every nonzero vector in $H$ is cyclic for $M$ , but no vector in $H$ is separating for $M$ .

Now let $ρ \in M$ be a faithful density matrix, meaning $ρ = ρ^{*}$ , $⟨ ρ v, v ⟩ > 0$ for every nonzero $v \in H$ , and $Tr (ρ) = 1$ . Let $K = M_{n} (C)$ with the Hilbert–Schmidt inner product $⟨ X, Y ⟩_{2} : = Tr (Y^{*} X),$ and represent $M$ on $K$ by left multiplication $L_{a} X : = a X$ . Then ${L_{a} : a \in M}$ is a concrete von Neumann algebra on $K$ , and $Ω : = ρ^{1 / 2}$ is a unit cyclic and separating vector for this representation. Its vector functional is $⟨ L_{a} Ω, Ω ⟩_{2} = Tr (ρ a) (a \in M) .$

Statement references

Concrete von Neumann algebra and faithful vector

Finite matrix spectral and state calculus

Hilbert–Schmidt operator and Hilbert–Schmidt norm

Facts & Assumptions

Given: Choice, $n > 1$ , $H = C^{n}$ , $M = M_{n} (C)$ , a faithful density matrix $ρ$ , and the finite matrix and Hilbert-space conventions.

[A1]

The Axiom of Choice is the declared hypothesis for the concrete von Neumann algebra interface (The Axiom of Choice, Concrete von Neumann algebra and faithful vector).

[F1]

The inner product is linear in its first argument, and Hilbert adjoints satisfy $⟨ A ξ, η ⟩ = ⟨ ξ, A^{*} η ⟩$ (Real and complex inner-product spaces and their induced length, Hilbert-adjoint identities).

[F2]

Finite Hermitian matrices have orthonormal eigenbases; positive square roots and their inverses exist for positive-definite matrices, and finite matrix trace is basis-independent and cyclic (Finite matrix spectral and state calculus, The basis-independent trace of an endomorphism of a finite-dimensional vector space).

[F3]

Relative to the standard orthonormal basis of $C^{n}$ , every $n \times n$ matrix is Hilbert–Schmidt, with squared Hilbert–Schmidt norm $\sum_{j} ∥ X e_{j} ∥^{2} = Tr (X^{*} X)$ (Hilbert–Schmidt operator and Hilbert–Schmidt norm, Hilbert space).

[F4]

A concrete von Neumann algebra is a unital star subalgebra equal to its double commutant; cyclic means dense orbit and separating means trivial operator kernel on the vector (Concrete von Neumann algebra and faithful vector).

[F5]

$B (H)$ denotes bounded linear operators with the operator norm (The spaces (\mathcal B(X,Y)) and (\mathcal B(X)) of bounded linear operators, A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[F6]

Finite scalar sums satisfy Cauchy–Schwarz (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs).

Proof

technique · direct finite-dimensional construction

Given: [A1], [F1]–[F6], and the matrices in the Statement.

1.1A1F4F5givenalgebra

Let $(e_{j})_{j = 1}^{n}$ be the standard orthonormal basis. If $T \in M^{'}$ , then commuting with each coordinate projection $P_{j}$ forces $T e_{j} = λ_{j} e_{j}$ . Commuting with each matrix unit $E_{i j}$ gives $λ_{i} = λ_{j}$ , hence $T = λ I$ . Conversely scalar matrices commute with every element of $M$ . Thus $M^{'} = C I$ and $M^{''} = (C I)^{'} = B (H) = M$ , so $M$ is concrete.

1.2F1F4givenconstruct

Fix $ξ \neq 0$ . For any $η \in H$ , define $a_{η} z : = ⟨ z, ξ ⟩ η / ∥ ξ ∥^{2}$ . This is a linear matrix operator and $a_{η} ξ = η$ , so $M ξ = H$ and $ξ$ is cyclic. If $ξ \neq 0$ , the orthogonal projection onto $ξ^{⊥}$ is nonzero since $n > 1$ , and it annihilates $ξ$ . If $ξ = 0$ , the identity is nonzero and annihilates $ξ$ . Hence no vector is separating for $M$ .

1.3F2F3givenconstruct

Direct matrix-unit calculation gives $⟨ E_{i j}, E_{k l} ⟩_{2} = δ_{i k} δ_{j l}$ , so the units are an orthonormal basis of $K$ . For $X = (x_{i j})$ , $∥ X ∥_{2}^{2} = \sum_{i, j} ∣ x_{i j} ∣^{2}$ , proving positive definiteness. If $(X_{m})$ is Cauchy, then each entry is Cauchy because $∣ x_{i j}^{(m)} - x_{i j}^{(k)} ∣ \leq ∥ X_{m} - X_{k} ∥_{2}$ . Their finitely many limits form a matrix $X$ , and the finite sum formula gives $∥ X_{m} - X ∥_{2} \to 0$ . Thus $K$ is complete and hence a Hilbert space; [F3] makes every matrix Hilbert–Schmidt.

2.1A1F1F4F5F6step 1.3givenalgebra

For $a, b \in M$ , the coordinate formulas are $(a X)_{i j} = \sum_{k} a_{i k} x_{k j}$ and $(X b)_{i j} = \sum_{k} x_{i k} b_{k j}$ . Finite Cauchy–Schwarz, summed over $i, j$ , gives $∥ a X ∥_{2}^{2} \leq (\sum_{i, k} ∣ a_{i k} ∣^{2}) ∥ X ∥_{2}^{2}$ and $∥ X b ∥_{2}^{2} \leq ∥ X ∥_{2}^{2} (\sum_{k, j} ∣ b_{k j} ∣^{2})$ . Thus $L_{a}, R_{b} \in B (K)$ by [F5] and [F6]. Also $L_{a} L_{b} = L_{a b}$ , $L_{I} = I_{K}$ , and $⟨ L_{a} X, Y ⟩_{2} = Tr (Y^{*} a X) = ⟨ X, L_{a^{*}} Y ⟩_{2}$ , so $L_{a}^{*} = L_{a^{*}}$ . Since $L_{a} I = a$ , the map $a \mapsto L_{a}$ is injective. If $S \in {L_{a} : a \in M}^{'}$ and $b = S (I)$ , then every $X = L_{X} (I)$ satisfies $S (X) = S (L_{X} I) = L_{X} S (I) = X b$ ; hence $S = R_{b}$ . Conversely every right multiplication commutes with every left multiplication. If $T \in {R_{b} : b \in M}^{'}$ and $a = T (I)$ , then every $X = R_{X} (I)$ satisfies $T (X) = R_{X} T (I) = a X$ , so $T = L_{a}$ ; the converse commutation also holds. Therefore ${L_{a} : a \in M}^{''} = {L_{a} : a \in M}$ , proving that the left representation is concrete.

3.1F2F4step 1.3step 2.1algebra

By [F2], $ρ^{1 / 2}$ is invertible and $∥ Ω ∥_{2}^{2} = Tr (ρ) = 1$ . For every $X \in K$ , $a = X ρ^{- 1 / 2}$ satisfies $L_{a} Ω = X$ , so $M Ω = K$ and $Ω$ is cyclic. If $L_{a} Ω = 0$ , then $a ρ^{1 / 2} = 0$ ; right multiplication by $ρ^{- 1 / 2}$ gives $a = 0$ , so $Ω$ is separating. Finally, $⟨ L_{a} Ω, Ω ⟩_{2} = Tr (ρ^{1 / 2} a ρ^{1 / 2}) = Tr (ρ a)$ by cyclicity of finite matrix trace [F2].

4.1step 1.1step 1.2step 1.3step 2.1step 3.1∎

Steps 1.1–1.2 establish the defining-representation assertions; steps 1.3, 2.1, and 3.1 construct the Hilbert–Schmidt left representation and verify its faithful cyclic-separating vector. The two representations act on different Hilbert spaces.