LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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.

Trace distance is unchanged by a fixed tensor factor

Statement

For density operators $ρ, σ$ on $H$ and $τ$ on $K$ , $D (ρ \otimes τ, σ \otimes τ) = D (ρ, σ)$ .

Facts & Assumptions

Given: Finite-dimensional complex inner-product spaces $H, K$ , density operators $ρ, σ$ on $H$ , and a density operator $τ$ on $K$ .

[F1]

Density operator: A density operator on $H$ is a non-negative endomorphism $ρ : H \to H$ with $tr (ρ) = 1$ .

[F2]

The product basis is orthonormal and tensor dimensions multiply: The elementary tensors of the factor bases, ordered lexicographically, form an orthonormal basis of the tensor register, and its dimension is the product of the dimensions.

[F3]

Trace Norm Spectral Formula: For every linear map $A : H \to K$ , $∥ A ∥_{1} = {tr}_{H} (\sqrt{A^{*} A})$ .

[F4]

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: A linear endomorphism $T$ of a finite-dimensional real or complex inner-product space is non-negative if and only if some orthonormal basis makes its matrix diagonal with nonnegative real diagonal entries.

[F5]

Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space: Every self-adjoint endomorphism is normal, because $T T^{*} = T^{2} = T^{*} T$ .

[F6]

Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely: Then $T$ is normal if and only if $V$ has an orthonormal basis consisting of eigenvectors of $T$ .

[F7]

A non-negative operator has a unique non-negative square root: For a non-negative endomorphism $T$ of a finite-dimensional real or complex inner-product space $V$ , there exists a unique non-negative operator $R : V \to V$ such that $R^{2} = T$ .

[F8]

Trace Distance: Their trace distance is $D (ρ, σ) : = \frac{1}{2} ∥ ρ - σ ∥_{1}$ .

[F9]

The basis-independent trace of an endomorphism of a finite-dimensional vector space: Choose any ordered basis $B$ of $V$ and define the trace by $tr (T) : = tr ([T]_{B}^{B})$ ; this is independent of the chosen basis.

[F10]

Tensor products of finitely many linear maps: A tensor map is the unique linear map whose action on elementary tensors applies each factor map to its corresponding factor.

[F11]

Tensor maps preserve composition, identities, and adjoints: Tensor maps preserve factorwise composition and adjoints: $(⨂_{k} S_{k}) (⨂_{k} T_{k}) = ⨂_{k} (S_{k} T_{k})$ and $(⨂_{k} T_{k})^{*} = ⨂_{k} T_{k}^{*}$ .

Proof

technique · direct

1.1givenF1F2F4F5F6F9F10choose

By [F4], [F2], and [F10], tensor products of orthonormal eigenbases diagonalize the tensor maps $ρ \otimes τ$ and $σ \otimes τ$ with nonnegative eigenvalues whose sums are $tr (ρ) tr (τ) = 1$ and $tr (σ) tr (τ) = 1$ , respectively; hence both are density operators. The difference $Δ = ρ - σ$ is self-adjoint, hence normal by [F5], and has an orthonormal eigenbasis $(e_{i})$ with real eigenvalues $λ_{i}$ by [F6]. Choose an orthonormal eigenbasis $(f_{j})$ for $τ$ with eigenvalues $t_{j} \geq 0$ and $\sum_{j} t_{j} = 1$ .

2.1step 1.1F2F3F7F8F10F11algebra∎

The product vectors $e_{i} \otimes f_{j}$ form an orthonormal basis by [F2], and [F10] shows that $Δ \otimes τ$ is diagonal there with real eigenvalues $λ_{i} t_{j}$ ; therefore it is self-adjoint. In agreement, [F11] gives $(Δ \otimes τ)^{*} = Δ^{*} \otimes τ^{*} = Δ \otimes τ$ . Applying the composition rule in [F11], its product with its adjoint is $(Δ^{*} Δ) \otimes (τ^{*} τ)$ , diagonal in this basis with entries $(λ_{i} t_{j})^{2}$ . Its unique nonnegative square root therefore has entries $∣ λ_{i} ∣ t_{j}$ by [F7]. The same computation on $(e_{i})$ gives $∥ Δ ∥_{1} = \sum_{i} ∣ λ_{i} ∣$ . Therefore [F3] gives $∥ Δ \otimes τ ∥_{1} = \sum_{i, j} ∣ λ_{i} ∣ t_{j} = \sum_{i} ∣ λ_{i} ∣ = ∥ Δ ∥_{1}$ . Dividing by two and using [F8] proves $D (ρ \otimes τ, σ \otimes τ) = D (ρ, σ)$ .

Depends on

Used by

Entanglement-free, randomness-free quantum fingerprints require Ω(log n) qubits Theorem

Dependency tree · two levels

43 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)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)