Alphabeta MathHow 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 Spectral Formula
Statement
For every linear map (Linear map between vector spaces over the same field) between finite-dimensional complex inner-product spaces,
Here and its non-negative square root are endomorphisms of the domain ; the trace is taken on .
Facts & Assumptions
Given: Finite-dimensional complex inner-product spaces and a linear map .
The singular values of are the eigenvalues of , counted with multiplicity (The singular values of a linear map as the eigenvalues of the positive square root of T^*T).
A non-negative operator has an orthonormal eigenbasis with nonnegative eigenvalues (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 trace of an endomorphism is the sum of its diagonal entries in any ordered basis, and the trace on the zero space is (The basis-independent trace of an endomorphism of a finite-dimensional vector space).
The trace norm is the sum of the singular values on the domain, including zeros (Trace Norm).
Proof
The operator in [F1] is non-negative. By [F2], choose an orthonormal eigenbasis of ; its eigenvalues, with multiplicity, are exactly the singular values of by [F1]. In that basis [F3] gives .
The sum in step 1.1 is by [F4]. If , both are the empty sum by [F3]–[F4]. This proves the formula for rectangular maps and all finite dimensions.
Depends on
- Linear map between vector spaces over the same field
- Trace Norm
- The singular values of a linear map as the eigenvalues of the positive square root of T^*T
- 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
Used by
- Acceptance probability weights an otherwise imperfect one-bit key Example
- Secrecy and correctness are separate requirements Example
- Partial trace contracts the trace norm on Hermitian operators Lemma
- Partial trace contracts trace distance Lemma
- Pure-state trace distance is bounded by vector error Lemma
- Trace distance is unchanged by a fixed tensor factor Lemma
- Trace norm of a finite classical block operator Lemma
- Entanglement-free, randomness-free quantum fingerprints require Ω(log n) qubits Theorem
- Full Rank Pair No Broadcasting Theorem
- Hermitian Trace Norm Positive Negative Parts Theorem
Cited to discharge well-definedness by Trace Norm.
Dependency tree · two levels
19 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.3, Eq. (1.181) (standard reference, not scraped)
- Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (2026-08-27), Appendix A.5 (standard reference, not scraped)