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.
Pauli six-outcome tomography
Example
On , define the Pauli matrices
Let , let , and let denote the diagonal-sum trace. For , write . For , means and for every . A finite POVM is a finite family of positive semidefinite matrices whose sum is ; it is informationally complete when its real linear span is . The six matrices , with , form such an informationally complete POVM. For every with and , there are unique such that . Define ; then . Form and the canonical duals as in the preceding finite-frame definition. The linear-inversion procedure returns on a valid frequency vector, meaning and . It returns when . Some valid finite frequency vectors yield an output that is not positive semidefinite.
Example references
Facts & Assumptions
Given: The six displayed matrices and a density matrix on .
The Pauli matrices and effects are the finite matrices and operators in the Example.
is Hermitian, positive semidefinite, and has trace one.
Tomography correctness and finite-sample stability: for a spanning finite POVM, exact probabilities reconstruct , and the linear-inversion output is for its canonical dual.
The Gram pseudoinverse reconstructs a spanning Hermitian frame: for a positive semidefinite Gram matrix with spectral projections at positive eigenvalues, .
Verification
Direct multiplication gives , , , , and ; reversing the order negates each mixed product. Thus . Since a Hermitian matrix has two real diagonal entries and one complex off-diagonal entry, ; the four nonzero orthogonal matrices form a basis. Write in this basis. Since and , the trace-one condition gives ; pairing with gives . Thus the representation is unique with . Write and . Positivity [A2] restricts , since and the eigenvalues of are .
Each is Hermitian with eigenvalues by step 1.1, so has eigenvalues and is positive. For each , ; summing over gives . Also , so each lies in the real span of the effects. Since is their sum, the basis in step 1.1 shows that the effects span .
In the coordinate order , direct multiplication and step 1.1 give for . Thus the diagonal entries are , opposite outcomes on one axis have entry , and distinct axes have entry . Let and . Then , , and vanishes on vectors with . These mutually orthogonal subspaces have dimensions and span .
By [F2] and the eigenspaces in step 3.1, , where and . The column of is . Applying the canonical-dual formula [F3], using and , gives ; similarly . The probabilities are , so , in agreement with [F1].
The frequency vector with and all other entries zero is nonnegative and sums to one. Its output is , whose eigenvalues are and . It is Hermitian but not positive, so the linear-inversion procedure does not preserve positivity for every frequency vector.