TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-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.

Trace Norm Rank One Formula

Statement

Let $H, K$ be finite-dimensional complex inner-product spaces, $x \in K$ , $y \in H$ , and $∣ x ⟩ ⟨ y ∣ : H \to K$ the rank-one linear map (Linear map between vector spaces over the same field) from Dirac Notation Conversion. Then

$∥ ∣ x ⟩ ⟨ y ∣ ∥_{1} = ∥ x ∥ ∥ y ∥ .$

Facts & Assumptions

Given: Finite-dimensional complex inner-product spaces $H, K$ and vectors $x \in K$ , $y \in H$ .

[F1]

The rank-one map acts by $A z = ⟨ z, y ⟩_{H, r o o t} x$ (Dirac Notation Conversion).

[F2]

The root inner product is linear in the first argument, conjugate-linear in the second, and $∥ v ∥^{2} = ⟨ v, v ⟩$ with $∥ v ∥ \geq 0$ (Real and complex inner-product spaces and their induced length).

[F3]

The adjoint is characterized by $⟨ T v, w ⟩ = ⟨ v, T^{*} w ⟩$ , and finite-dimensional adjoints exist uniquely (The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ , Every linear map between finite-dimensional inner product spaces has a unique adjoint).

[F4]

Singular values are the eigenvalues, with multiplicity, of $∣ A ∣ = \sqrt{A^{*} A}$ (The singular values of a linear map as the eigenvalues of the positive square root of T^*T).

[F5]

A self-adjoint operator with nonnegative eigenvalues is non-negative; every non-negative operator has a unique non-negative square root (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 non-negative operator has a unique non-negative square root).

[F6]

The trace norm sums all domain singular values (Trace Norm).

Proof

1.1givenF1F2F6

If $x = 0$ or $y = 0$ , [F1] makes $A = ∣ x ⟩ ⟨ y ∣$ the zero map. Then [F6] gives $∥ A ∥_{1} = 0$ , while [F2] gives $∥ x ∥ ∥ y ∥ = 0$ .

1.2F1F2F3algebra

Suppose $x, y \neq 0$ . For $z \in H$ and $w \in K$ , [F1]–[F2] give $⟨ A z, w ⟩_{K} = ⟨ z, y ⟩_{H} ⟨ x, w ⟩_{K} = ⟨ z, ⟨ w, x ⟩_{K} y ⟩_{H} .$ Thus the adjoint identity [F3] gives $A^{*} w = ⟨ w, x ⟩_{K} y$ , and therefore $A^{*} A z = ∥ x ∥^{2} ⟨ z, y ⟩_{H} y$ .

2.1F2step 1.2algebra

Let $e = y / ∥ y ∥$ and put $λ = ∥ x ∥^{2} ∥ y ∥^{2}$ . Step 1.2 gives $A^{*} A e = λ e$ and $A^{*} A z = 0$ whenever $z ⊥ e$ . Every $z \in H$ has the decomposition $z = ⟨ z, e ⟩ e + (z - ⟨ z, e ⟩ e)$ , whose second term is orthogonal to $e$ ; the two summands intersect only at $0$ . Therefore $H = span {e} \oplus e^{⊥}$ , and $A^{*} A$ acts by $λ$ on the first summand and by $0$ on the second.

3.1F2F4F5F6step 1.1step 2.1algebra∎

Define $R$ on the direct sum $H = span {e} \oplus e^{⊥}$ by $R e = ∥ x ∥ ∥ y ∥ e$ and $R z = 0$ for $z ⊥ e$ , extending linearly. For $z, w \in H$ , put $c = ⟨ z, e ⟩$ and $d = ⟨ w, e ⟩$ . Then $⟨ R z, w ⟩ = ∥ x ∥ ∥ y ∥ c \overline{d} = ⟨ z, R w ⟩$ , so $R$ is self-adjoint; its eigenvalues are $∥ x ∥ ∥ y ∥$ on $span {e}$ and $0$ on $e^{⊥}$ . These eigenvalues are nonnegative, so [F5] makes $R$ non-negative. It satisfies $R^{2} = A^{*} A$ by step 2.1. Uniqueness in [F5] gives $R = ∣ A ∣ = \sqrt{A^{*} A}$ . Its eigenvalues are $∥ x ∥ ∥ y ∥$ once and $0$ on $e^{⊥}$ , so [F4] and [F6] give $∥ A ∥_{1} = ∥ x ∥ ∥ y ∥$ . Together with step 1.1 this proves the formula, including zero vectors and zero-dimensional spaces.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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 (2018 author-hosted draft), Chapter 1, §§1.1.1–1.1.3 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (2026-08-27), Appendices A.5 and A.10 (standard reference, not scraped)