LemmaStatement: AI-adaptedProof: AI-adapted

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.

Pure-state separability is equivalent to being a product: a Schmidt overlap witness

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H, K$ be arbitrary nonzero complex Hilbert spaces, with inner products linear in the first argument, and put $L = H \hat{\otimes} K$ with the isometric inclusion $κ$ of Hilbert tensor construction: inner product, completion and product bases. Write $T_{x, y} z = ⟨ z, y ⟩ x$ as in Rank-one operator calculus. Set $P = {T_{κ (a \otimes b), κ (a \otimes b)} : ∥ a ∥ = ∥ b ∥ = 1}, S = {\overline{conv P}}^{∥ \cdot ∥_{1}},$ with trace class as in Trace class operator, where the convex hull consists of finite convex combinations, and the closure is taken in the trace-class operators on $L$ . For each unit $Ψ \in L$ , let $P_{Ψ} = T_{Ψ, Ψ}$ . Then $P_{Ψ} \in S ⟺ Ψ = κ (a \otimes b) for some unit a \in H, b \in K .$

More precisely, let $Ψ = \sum_{r \in J} s_{r} κ (v_{r} \otimes u_{r})$ be any finite or countably infinite positive Schmidt expansion from Infinite Schmidt decomposition and the pure product criterion, and put $λ_{r} = s_{r}^{2}$ . The number $m = \max_{r \in J} λ_{r}$ exists. Every pair of unit vectors $a, b$ satisfies $∣ ⟨ Ψ, κ (a \otimes b) ⟩ ∣^{2} \leq m$ , with equality at a Schmidt pair whose weight is $m$ . Every $σ \in S$ satisfies $tr (σ P_{Ψ}) \leq m$ , whereas $tr (P_{Ψ}^{2}) = 1$ . If $Ψ$ is non-product then $m < 1$ and, for every $σ \in S$ , $∥ P_{Ψ} - σ ∥_{1} \geq 1 - m > 0.$ The factors need not be separable; only the support of the single tensor vector has a countable Schmidt expansion. These are mathematical trace pairings, with no measurement or Born-rule assumption.

Facts & Assumptions

Given: Countable Choice; the Hilbert spaces $H, K$ ; $L$ , $κ$ , $P$ , $S$ and unit $Ψ$ as above.

[F1]

The completed tensor product is Hilbert, $∥ κ (a \otimes b) ∥ = ∥ a ∥ ∥ b ∥$ , and $⟨ κ (x \otimes y), κ (a \otimes b) ⟩ = ⟨ x, a ⟩ ⟨ y, b ⟩$ , with linearity in the first argument (Hilbert tensor construction: inner product, completion and product bases clauses (a), (c)).

[F2]

Under Countable Choice, an arbitrary unit tensor vector has a nonempty at most countable positive Schmidt expansion, with orthonormal families $(v_{r})$ , $(u_{r})$ and $\sum_{r} s_{r}^{2} = 1$ ; it is a product vector exactly when there is one positive coefficient (Infinite Schmidt decomposition and the pure product criterion, Statement). No ambient Hilbert basis is assumed.

[F3]

Rank-one operators are positive when their two vectors agree, have trace $tr T_{x, y} = ⟨ x, y ⟩$ , and for trace-class $T$ satisfy $tr (T T_{x, y}) = ⟨ T x, y ⟩$ . Trace is linear by Trace is absolutely convergent and basis independent clause 4, and $∥ T ∥ \leq ∥ T ∥_{1}$ by Trace class is a two sided Banach operator ideal clause 1; the rank-one identities are Rank-one operator calculus clauses (b), (c), (e).

Proof

Given: The data of the statement and [F1]–[F3].

1.1givenF2algebra

[Maximum and the strict gap] By [F2], $λ_{r} > 0$ and $\sum_{r} λ_{r} = 1$ . Fix one $r_{0} \in J$ and put $c = λ_{r_{0}} > 0$ . The set $E = {r : λ_{r} \geq c}$ is nonempty and finite: any finite subset of $E$ with $N$ elements has weight sum at least $N c \leq 1$ , so $E$ has at most $⌊ 1 / c ⌋$ elements. The maximum $m$ on this finite set is a maximum on $J$ , since every weight outside $E$ is below $c \leq m$ . If $Ψ$ is non-product, [F2] gives at least two positive weights; at an index $r_{*}$ attaining $m$ , another positive weight implies $m < \sum_{r} λ_{r} = 1$ .

1.2givenF1algebra

[Finite orthogonal estimates] For an orthonormal family $(e_{r})$ , a vector $x$ and a finite set $F$ , expanding $∥ x - \sum_{r \in F} ⟨ x, e_{r} ⟩ e_{r} ∥^{2}$ gives $∥ x ∥^{2} - \sum_{r \in F} ∣ ⟨ x, e_{r} ⟩ ∣^{2} \geq 0$ . Thus for unit $a, b$ the sums of $∣ ⟨ v_{r}, a ⟩ ∣^{2}$ and $∣ ⟨ u_{r}, b ⟩ ∣^{2}$ are each at most one, using conjugate symmetry and the supremum of finite sums. For finite complex sequences $(α_{r}), (β_{r})$ , Cauchy–Schwarz gives $∣ \sum_{r} α_{r} β_{r} ∣ \leq (\sum_{r} ∣ α_{r} ∣^{2})^{1 / 2} (\sum_{r} ∣ β_{r} ∣^{2})^{1 / 2}$ : this follows by expanding $\sum_{r} ∣ α_{r} - t \overline{β_{r}} ∣^{2} \geq 0$ with $t = (\sum_{r} α_{r} β_{r}) / (\sum_{r} ∣ β_{r} ∣^{2})$ when the denominator is positive, and is immediate otherwise.

1.3givenF3algebra

[Exact continuity of the fixed trace witness] For every trace-class $T$ on $L$ , [F3] gives $tr (T P_{Ψ}) = ⟨ T Ψ, Ψ ⟩$ and $∣ tr (T P_{Ψ}) ∣ \leq ∥ T Ψ ∥ ∥ Ψ ∥ \leq ∥ T ∥ \leq ∥ T ∥_{1}$ , since $∥ Ψ ∥ = 1$ . Applying this estimate to $T - S$ proves $∣ tr (T P_{Ψ}) - tr (S P_{Ψ}) ∣ \leq ∥ T - S ∥_{1}$ . Thus this particular bounded trace functional is 1-Lipschitz; no unspecified continuity theorem or unbounded cyclicity is used. Also $P_{Ψ} Ψ = Ψ$ , so $tr (P_{Ψ}^{2}) = ⟨ P_{Ψ} Ψ, Ψ ⟩ = 1$ .

2.1step 1.1step 1.2F1F2algebra

[The overlap bound, with the conjugations fixed] For a finite Schmidt truncation $Ψ_{F}$ , [F1] gives $⟨ Ψ_{F}, κ (a \otimes b) ⟩ = \sum_{r \in F} s_{r} ⟨ v_{r}, a ⟩ ⟨ u_{r}, b ⟩$ ; equivalently it is the conjugate of $\sum_{r \in F} s_{r} ⟨ a, v_{r} ⟩ ⟨ b, u_{r} ⟩$ . Applying step 1.2 to $α_{r} = s_{r} ⟨ v_{r}, a ⟩$ and $β_{r} = ⟨ u_{r}, b ⟩$ gives a modulus bound $(\sum_{r \in F} λ_{r} ∣ ⟨ v_{r}, a ⟩ ∣^{2})^{1 / 2} (\sum_{r \in F} ∣ ⟨ u_{r}, b ⟩ ∣^{2})^{1 / 2} \leq \sqrt{m}$ . The Schmidt truncations converge in norm [F2], so continuity of the Hilbert pairing passes this bound to $Ψ$ . At $a = v_{r_{*}}$ and $b = u_{r_{*}}$ , orthonormality gives overlap $s_{r_{*}}$ and squared overlap $m$ .

3.1step 2.1step 1.3F3algebra

[Convex hull and its closure] For unit product $q = κ (a \otimes b)$ , [F3] and first-linear conjugate symmetry give $tr (T_{q, q} P_{Ψ}) = ⟨ T_{q, q} Ψ, Ψ ⟩ = ⟨ Ψ, q ⟩ ⟨ q, Ψ ⟩ = ∣ ⟨ Ψ, q ⟩ ∣^{2} \leq m$ by step 2.1. Trace linearity gives the same real bound for finite convex combinations. For $σ \in S$ and every $ε > 0$ , the definition of closure supplies a single $τ \in conv P$ with $∥ σ - τ ∥_{1} < ε$ . Step 1.3 gives $∣ tr (σ P_{Ψ}) - tr (τ P_{Ψ}) ∣ < ε$ ; letting $ε ↓ 0$ shows that $tr (σ P_{Ψ})$ is real and at most $m$ . This neighborhood argument does not select a sequence of approximants.

4.1step 1.1step 1.3step 3.1F1algebra∎

[Equivalence and distance] If $Ψ$ is non-product, steps 1.1, 1.3 and 3.1 give $tr (P_{Ψ}^{2}) = 1 > m \geq tr (σ P_{Ψ})$ for all $σ \in S$ , so $P_{Ψ} \notin S$ . Moreover step 1.3 gives $∥ P_{Ψ} - σ ∥_{1} \geq ∣ tr ((P_{Ψ} - σ) P_{Ψ}) ∣ = 1 - tr (σ P_{Ψ}) \geq 1 - m$ . Conversely a unit product vector has $P_{Ψ} \in P \subseteq S$ . If initially $Ψ = κ (x \otimes y)$ with arbitrary nonzero factors, [F1] gives $∥ x ∥ ∥ y ∥ = 1$ ; therefore $a = x / ∥ x ∥$ and $b = ∥ x ∥ y$ are unit and $Ψ = κ (a \otimes b)$ . This proves the full claimed equivalence for the declared trace-norm closure and the strict witness bound.

Depends on

Dependency tree · 2 levels

Sources

MIT 8.05 Quantum Physics II (Fall 2013), Chapter 8, Section 2: product and entangled pure vectors; the closed-convex-hull equivalence is proved locally here