LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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.

Positive Marginals Imply Joint Support

Statement

Let $H$ be finite-dimensional, let $Y \geq 0$ act on $H \otimes H$ , and let $S \subseteq H$ be a subspace. If both partial-trace marginals of $Y$ are supported on $S$ , then $supp Y \subseteq S \otimes S$ ; equivalently, $Y = (P_{S} \otimes P_{S}) Y (P_{S} \otimes P_{S})$ , where $P_{S}$ is the orthogonal projection onto $S$ .

Facts & Assumptions

Given: A finite-dimensional complex Hilbert space $H$ , $Y \geq 0$ on $H \otimes H$ , a subspace $S \subseteq H$ , and $supp ({Tr}_{2} Y), supp ({Tr}_{1} Y) \subseteq S$ .

[F1]

For any non-negative finite-dimensional operator $Z$ , define $supp (Z) : = (\ker Z)^{⊥} = range (Z)$ ; equality follows from self-adjointness (A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S).

[L1]

The partial trace is characterized by $tr (({Tr}_{B} R) T) = tr (R (T \otimes I))$ , independently of the auxiliary orthonormal basis (Partial trace over a finite tensor factor, The partial trace is characterized by the trace pairing and is basis-independent). The QC02 definition and characterization theorem are present as draft carriers; the trace-pairing identity gives the displayed marginal trace rule by cyclicity.

[L2]

$P_{S}$ is the orthogonal projection onto $S$ ; it is idempotent and $Q = I - P_{S} = P_{S^{⊥}}$ . It is self-adjoint because the orthogonal decomposition gives $⟨ P_{S} x, y ⟩ = ⟨ P_{S} x, P_{S} y ⟩ = ⟨ x, P_{S} y ⟩$ for all $x, y$ (The orthogonal projection $P_{W} v$ is the $W$ -component in $V = W \oplus W^{⊥}$ , Orthogonal projection is linear, and an orthonormal basis $(e_{i})$ of $W$ gives $P_{W} v = \sum_{i} ⟨ v, e_{i} ⟩ e_{i}$ ). Hence $Q^{*} = Q$ and $Q^{2} = Q$ .

[L3]

Tensor maps act factorwise and preserve composition, so operators acting on different tensor factors commute and $(P_{S} \otimes I) (I \otimes P_{S}) = P_{S} \otimes P_{S}$ (Tensor products of finitely many linear maps, Tensor maps preserve composition, identities, and adjoints).

[F2]

A non-negative operator has a unique non-negative square root (A non-negative operator has a unique non-negative square root). If such an operator has trace zero, diagonalize it in an orthonormal eigenbasis with nonnegative eigenvalues; trace is their sum, so every eigenvalue is zero and the operator is zero (A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S, The basis-independent trace of an endomorphism of a finite-dimensional vector space).

Proof

1.1givenF1L1L2F2algebra

Let $Q = I - P_{S}$ . By [F1], the range of ${Tr}_{2} Y$ lies in $S$ , so $Q {Tr}_{2} Y = 0$ and $tr (Q {Tr}_{2} Y) = 0$ . By [L1], $tr ((Q \otimes I) Y) = 0$ . Cyclicity of trace rewrites this as $tr (Y^{1 / 2} (Q \otimes I) Y^{1 / 2}) = 0$ . Since [L2] gives $(Q \otimes I)^{*} = (Q \otimes I)^{2} = Q \otimes I$ , the operator inside the trace is $Z^{*} Z \geq 0$ for $Z = (Q \otimes I) Y^{1 / 2}$ ; [F2] makes it zero, hence $Z = 0$ because $⟨ Z^{*} Z v, v ⟩ = ∥ Z v ∥^{2}$ . Thus $(Q \otimes I) Y = Y (Q \otimes I) = 0$ , and $Y = (P_{S} \otimes I) Y (P_{S} \otimes I)$ .

2.1givenstep 1.1L1L2F2

Applying the same argument to the second marginal with the projection $I \otimes Q$ gives $Y = (I \otimes P_{S}) Y (I \otimes P_{S})$ .

3.1step 1.1step 2.1L2L3algebra∎

The two commuting projections $P_{S} \otimes I$ and $I \otimes P_{S}$ have product $P_{S} \otimes P_{S}$ by [L3]. Combining step 1.1 and step 2.1 yields $Y = (P_{S} \otimes P_{S}) Y (P_{S} \otimes P_{S})$ , so the range and hence the support of $Y$ lies in $S \otimes S$ .

Depends on

Used by

Singular Pair No Broadcasting Theorem

Dependency tree · two levels

45 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John Watrous, The Theory of Quantum Information (standard reference, not scraped)