TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Infinite Schmidt decomposition and the pure product criterion

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) and let $H, K$ be nonzero complex Hilbert spaces (Hilbert space) with $H \hat{\otimes} K$ their completed tensor product (Hilbert tensor construction: inner product, completion and product bases). A product vector means an elementary tensor $v \otimes u$ with $v \in H$ and $u \in K$ . Then for every $Ψ \in H \hat{\otimes} K$ there are an at most countable index set $J$ , orthonormal families $(v_{r})_{r \in J} \subseteq H$ and $(u_{r})_{r \in J} \subseteq K$ , and numbers $s_{r} > 0$ with

$Ψ = \sum_{r \in J} s_{r} v_{r} \otimes u_{r} (norm convergence in H \hat{\otimes} K),$

and $∥ Ψ ∥^{2} = \sum_{r} s_{r}^{2}$ . The $s_{r}$ are the positive square roots of the nonzero eigenvalues of $C C^{*}$ , where $C : \overline{K_{0}} \to H_{0}$ is the linear coefficient operator on countable closed factor supports of $Ψ$ , defined below; if $J$ is infinite then $s_{r} \to 0$ . For $∥ Ψ ∥ = 1$ the reduced density $ρ = {Tr}_{K} T_{Ψ, Ψ}$ has $tr ρ^{2} = \sum_{r} s_{r}^{4}$ , and $tr ρ^{2} = 1$ holds exactly when exactly one $s_{r}$ is nonzero, i.e. exactly when $Ψ$ is a product vector. No assertion about separability of mixed density operators is made here.

For clarity, choose finite algebraic tensors converging to $Ψ$ and let $H_{0} \subseteq H$ , $K_{0} \subseteq K$ be the closed spans of their factor vectors. These supports have finite/countable orthonormal bases, and $Ψ \in H_{0} \hat{\otimes} K_{0}$ . The conjugate Hilbert space $\overline{K_{0}}$ consists of symbols $\overset{ˉ}{z}$ , with $a \overset{ˉ}{z} : = \overline{\overset{ˉ}{a} z}$ and $⟨ \overset{ˉ}{z}, \overset{ˉ}{w} ⟩_{\overline{K_{0}}} : = ⟨ w, z ⟩_{K_{0}}$ . For an orthonormal basis $(f_{j})$ of $K_{0}$ , write $Ψ = \sum_{j} h_{j} \otimes f_{j}$ and set $C {\overset{ˉ}{f}}_{j} = h_{j}$ , extending linearly and continuously. The positive singular values and the nonzero spectrum of $C C^{*}$ are independent of these supports and bases, as the reduced-state identity proved below shows.

Facts & Assumptions

Given: Countable Choice, arbitrary nonzero complex Hilbert spaces $H, K$ , and $Ψ \in H \hat{\otimes} K$ . The supports, bases and coefficient map are constructed in the proof; no countable basis of the ambient spaces is assumed.

[F1]

Algebraic tensors are dense in their Hilbert completion, and orthogonal coordinates have the squared-norm sum formula. A given dense sequence in a Hilbert space yields a finite/countable orthonormal basis by Gram–Schmidt (Hilbert tensor construction: inner product, completion and product bases, A Hilbert space with a dense sequence has a finite or countable orthonormal basis, Parseval equivalences for an orthonormal family).

[F2]

Bounded finite-rank operators are compact, and an operator-norm limit of compact operators into a Hilbert space is compact under Countable Choice. Hilbert adjoints satisfy the adjoint identity and $(C^{*})^{*} = C$ ; Cauchy–Schwarz bounds coordinate sums (Bounded finite rank operators are compact, Norm limit of compact operators is compact, Hilbert-adjoint identities, Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs).

[F3]

A compact positive self-adjoint operator has positive eigenvalues of finite multiplicity, accumulating only at zero, and its nonzero eigenspaces span the orthogonal complement of its kernel. A positive trace-class operator has trace and trace norm equal to the sum of its positive eigenvalues (Spectral theorem for compact self adjoint operators, Trace of a positive operator is the sum of its eigenvalues).

[F4]

Rank-one operators have trace norm $∥ T_{u, v} ∥_{1} = ∥ u ∥ ∥ v ∥$ and trace $⟨ u, v ⟩$ . The partial trace is bounded in trace norm with the defining bounded-operator pairing and elementary rank-one formula. Bounded tensor maps extend with their norm and adjoint identities (Rank-one operator calculus, Separable partial trace and its basic properties, Bounded tensor maps: extension, norm estimate, adjoint and commutation, Trace class is a two sided Banach operator ideal).

Proof

1.1givenF1F4chooseconstructalgebra

[Countable supports and coefficients] By density and Countable Choice choose algebraic tensors $Ψ_{n} \to Ψ$ with finite factor decompositions. Their countably many factor vectors span closed subspaces $H_{0}, K_{0}$ with explicit dense sequences of finite rational complex combinations; [F1] supplies finite/countable orthonormal bases. The inclusion of $H_{0} ⊙ K_{0}$ in $H \hat{\otimes} K$ is isometric and extends to its closed completion, which contains $Ψ$ . Choose the basis $(f_{j})$ of $K_{0}$ . As in the orthogonal contraction construction of Separable partial trace and its basic properties, coefficient contractions define $h_{j} \in H_{0}$ with $Ψ = \sum_{j} h_{j} \otimes f_{j}$ and $\sum_{j} ∥ h_{j} ∥^{2} = ∥ Ψ ∥^{2}$ . All sums here may be finite or empty, including $Ψ = 0$ .

2.1step 1.1F1F2F4constructalgebra

[The typed compact coefficient operator] Define $C (\sum_{j} z_{j} {\overset{ˉ}{f}}_{j}) : = \sum_{j} z_{j} h_{j}$ first on finite sums in $\overline{K_{0}}$ . Cauchy–Schwarz gives $∥ C z ∥ \leq (\sum_{j} ∥ h_{j} ∥^{2})^{1 / 2} ∥ z ∥$ , so it extends to all of $\overline{K_{0}}$ by continuity and completeness. The finite truncations $C_{N}$ have finite rank and $∥ C - C_{N} ∥ \leq (\sum_{j > N} ∥ h_{j} ∥^{2})^{1 / 2} \to 0$ , so [F2] makes $C$ compact. The adjoint has the correctly typed formula $C^{*} x = \sum_{j} ⟨ x, h_{j} ⟩ {\overset{ˉ}{f}}_{j}$ for $x \in H_{0}$ , hence $C C^{*} x = \sum_{j} ⟨ x, h_{j} ⟩ h_{j}$ . The finite sums $\sum_{j \leq N} T_{h_{j}, h_{j}}$ converge in trace norm by [F4], with trace sum $\sum_{j} ∥ h_{j} ∥^{2}$ ; their operator-norm limit is $C C^{*}$ , so $C C^{*}$ is positive trace class with $tr C C^{*} = ∥ Ψ ∥^{2}$ .

3.1step 1.1step 2.1F4algebra

[Reduced-state identity] Let $Ψ_{N} = \sum_{j \leq N} h_{j} \otimes f_{j}$ . The elementary partial-trace formula gives ${Tr}_{K} T_{Ψ_{N}, Ψ_{N}} = \sum_{j \leq N} T_{h_{j}, h_{j}}$ , regarding the latter operators on $H$ as zero on $H_{0}^{⊥}$ . Rank-one continuity and boundedness of the partial trace [F4] pass to the limit and give ${Tr}_{K} T_{Ψ, Ψ} = C C^{*}$ extended by zero. Thus the nonzero eigenvalues of $C C^{*}$ are intrinsic to $Ψ$ , independent of all auxiliary supports and bases.

4.1step 2.1step 3.1F1F2F3chooseconstructalgebra

[Singular vectors in the conjugate factor] By [F3] choose orthonormal eigenvectors $v_{r} \in H_{0}$ for the positive eigenvalues $s_{r}^{2}$ of $C C^{*}$ , counted with multiplicity; finite-dimensional eigenspace bases are supplied by [F1] and their countable selection uses the stated Countable Choice. Define ${\overset{ˉ}{u}}_{r} : = s_{r}^{- 1} C^{*} v_{r} \in \overline{K_{0}}$ . Then $⟨ {\overset{ˉ}{u}}_{r}, {\overset{ˉ}{u}}_{t} ⟩ = s_{r}^{- 1} s_{t}^{- 1} ⟨ v_{r}, C C^{*} v_{t} ⟩ = δ_{r t}$ , so the actual vectors $u_{r} \in K_{0}$ are orthonormal too. By step 2.1 their coefficients obey $u_{r} = \sum_{j} s_{r}^{- 1} ⟨ h_{j}, v_{r} ⟩ f_{j}$ . The trace formula [F3] gives $\sum_{r} s_{r}^{2} = tr C C^{*} = ∥ Ψ ∥^{2}$ , and infinitely many positive eigenvalues tend to zero.

5.1step 1.1step 4.1F1F3algebra

[Reconstruction] If $g \in \ker C C^{*}$ then $0 = ⟨ C C^{*} g, g ⟩ = ∥ C^{*} g ∥^{2}$ , so all $⟨ g, h_{j} ⟩$ vanish. Thus every $h_{j}$ is in the closed span of the $v_{r}$ by [F3], and $h_{j} = \sum_{r} ⟨ h_{j}, v_{r} ⟩ v_{r}$ . The orthonormal series $\sum_{r} s_{r} v_{r} \otimes u_{r}$ converges in tensor norm because $\sum_{r} s_{r}^{2} < \infty$ . Its $f_{j}$ coefficient is $\sum_{r} s_{r} ⟨ u_{r}, f_{j} ⟩ v_{r} = \sum_{r} ⟨ h_{j}, v_{r} ⟩ v_{r} = h_{j}$ by step 4.1. The orthogonal coefficient norm formula [F1] therefore identifies its sum with $Ψ$ . If $Ψ = 0$ , the positive spectrum and the Schmidt family are empty, giving the zero expansion.

6.1step 2.1step 3.1step 4.1step 5.1F3F4algebra∎

[Purity and product criterion] For $∥ Ψ ∥ = 1$ , steps 3.1–5.1 show that the reduced density has eigenvalues $s_{r}^{2}$ and $\sum_{r} s_{r}^{2} = 1$ , hence $tr ρ^{2} = \sum_{r} s_{r}^{4}$ . The difference $(\sum_{r} s_{r}^{2})^{2} - \sum_{r} s_{r}^{4} = 2 \sum_{r < t} s_{r}^{2} s_{t}^{2}$ vanishes exactly when there is one positive coefficient. That case makes the expansion a product vector. Conversely for a nonzero product $a \otimes b$ , its coefficients are $h_{j} = ⟨ b, f_{j} ⟩ a$ , so $C$ has rank one and $C C^{*}$ has one positive eigenvalue; for a unit product its reduced purity is one. All ambient Hilbert spaces remain arbitrary; only the supports of this particular vector were made countable. This establishes every claimed clause.

Infinite Schmidt decomposition and the pure product criterion

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources