Verified Examples

The examples below verify specific finite matrix identities with exact symbolic arithmetic. They test conjugation, channel normalization, tensor ordering, and a negative complete-positivity witness. They are reproducible calculations, not proof-assistant kernel proofs or numerical simulations of arbitrary quantum systems. Their mathematical interpretation uses the stated matrix definitions and standard theorems linked below.

Required background. Pure States as Projectors defines rank-one states; Complete Positivity of Dynamics explains why positivity on isolated inputs is insufficient.

A complex projector tests conjugation

Take $v=(1,i)^T$ and $P=vv^*/2$. The vector has squared norm two, so $P$ should be Hermitian, idempotent, and trace one. Its off-diagonal entries are imaginary. Therefore replacing conjugate transpose by ordinary transpose changes the result, making this a useful test that a purely real example would miss.

The script checks all three projector identities and also checks that $P^T\ne P$. These statements concern the displayed matrix. The general rank-one projector theorem remains in its canonical treatment; a successful test on this $v$ is not a substitute for that theorem.

A Choi convention fixes the tensor ordering

For a qubit channel, use the unnormalized Choi operator

$$J(\Phi)=\sum_{i,j=0}^1 |i\rangle\langle j|\otimes\Phi(|i\rangle\langle j|).$$

The first factor labels the input reference and the second the output. Trace preservation is $\operatorname{Tr}_{\rm out}J=I$, so $\operatorname{Tr}J=2$, not one. The normalized Choi state would instead divide by the input dimension and change that marginal to $I/2$.

Set $Z=\operatorname{diag}(1,-1)$ and $\Phi(M)=\tfrac23M+\tfrac13ZMZ$. The script constructs $J$ by applying the map to all four matrix units. It then verifies its factorization

$$J=\tfrac23uu^*+\tfrac13ww^*, \quad u=(1,0,0,1)^T, \quad w=(1,0,0,-1)^T.$$

Positive weights and outer products certify positivity of this exact matrix; the output partial-trace check certifies normalization. The finite-dimensional Choi theorem connects those properties to complete positivity and trace preservation. The code explicitly implements the chosen convention rather than relying on an unstated reshape order.

A negative control distinguishes positive from completely positive

Apply the same Choi construction to transposition $T(M)=M^T$. For $a=(0,1,-1,0)^T$, the script finds $a^*J(T)a=-2$. Thus $J(T)$ is not positive, despite transposition preserving positivity of individual matrices. The normalized antisymmetric vector has expectation $-1$. This negative control catches a checker that merely tests Hermiticity, trace preservation, or positivity on a few isolated input states.

The canonical complete-positivity discussion explains the ancilla criterion. Here the exact witness is used as a small reproducible diagnostic, not as a new definition of positivity.

Reproduce the exact checks

Run the following Python script with SymPy installed. It uses rational entries and the exact imaginary unit; no floating-point tolerances enter the assertions. Use an ordinary Python invocation, since optimization mode can disable Python assert statements.

from sympy import I, Matrix, Rational, eye, zeros, kronecker_product

v = Matrix([1, I])
P = v * v.H / 2
assert P.H == P
assert P * P == P
assert P.trace() == 1
assert P.T != P

Z = Matrix([[1, 0], [0, -1]])

def matrix_unit(i, j):
    E = zeros(2)
    E[i, j] = 1
    return E

def choi(phi):
    J = zeros(4)
    for i in range(2):
        for j in range(2):
            E = matrix_unit(i, j)
            J += kronecker_product(E, phi(E))
    return J

def phi(M):
    return Rational(2, 3) * M + Rational(1, 3) * Z * M * Z

J = choi(phi)
u = Matrix([1, 0, 0, 1])
w = Matrix([1, 0, 0, -1])
assert J == Rational(2, 3) * u * u.H + Rational(1, 3) * w * w.H
assert J.H == J
trace_out = Matrix(2, 2, lambda i, j:
    sum(J[2 * i + b, 2 * j + b] for b in range(2)))
assert trace_out == eye(2)
assert J.trace() == 2

JT = choi(lambda M: M.T)
a = Matrix([0, 1, -1, 0])
assert (a.H * JT * a)[0] == -2
assert a.dot(a) == 2
print("Exact projector, channel, and negative-control checks passed.")

The displayed code was run with Python 3.13.7 and SymPy 1.13.3; all assertions passed. Its output is Exact projector, channel, and negative-control checks passed. The displayed source is the complete calculation. A reproduction should record Python and SymPy versions along with the unmodified source and exit status. A failed assertion is a failed check; suppressing it or replacing exact equality by a large tolerance would change what the calculation establishes.

What these checks leave unproved

The script trusts Python, SymPy, and their arithmetic implementation. It does not emit a proof term checked by Lean, Rocq, or Isabelle. It verifies the finite displayed instances rather than all channels, all dimensions, or an unbounded-operator limit. A formal port would state the matrix identities and prove them in the selected library, then inspect their dependencies as described in Proof Assistant Preview.

Exercise: detect a Choi normalization mismatch

Suppose a program returns $J/2$ but its test expects the output partial trace to be $I$. Which assertion fails, and which convention would make the returned object correct?

Solution

The partial trace becomes $I/2$, and the total trace becomes one, so both unnormalized-Choi assertions fail. The object is the normalized Choi state, which is a legitimate convention when its marginal condition is stated as $I/2$. Correcting the convention is different from changing the physical channel. The test should make that choice explicit.

References

• Choi, Man-Duen, “Completely positive linear maps on complex matrices,” Linear Algebra and its Applications 10, 285–290 (1975), doi:10.1016/0024-3795(75)90075-0 — the finite-dimensional positivity criterion.
• Meurer, Aaron, et al., “SymPy: symbolic computing in Python,” PeerJ Computer Science 3, e103 (2017), doi:10.7717/peerj-cs.103 — the symbolic computation system used in the reproducible example.
• Watrous, John, The Theory of Quantum Information, Cambridge University Press, 2018, doi:10.1017/9781316848142 — Choi conventions and channel interpretation.