12 The Half-Flip: CPT, Time Reversal, and Complete Positivity
The shadow involution squares to the identity on conformal dimensions. On states it does not: the antiunitary time-reversal operator \(T\) squares to \(-1\) on a spin-\(\tfrac 12\) system. That factor of \(-1\) — the “half-flip” — is what this chapter formalizes, together with its consequence that the operation is not a physically implementable channel.
12.1 Wigner time reversal squares to \(-1\)
\(T(\psi _1,\psi _2) := (\overline{\psi _2},\, -\overline{\psi _1})\).
\(T\psi \) is orthogonal to \(\psi \) for every \(\psi \).
\(T(T\psi ) = -\psi \). Proved clean. This is the half-flip itself: applying time reversal twice returns the state up to a global sign, so \(T\) generates a \(\mathbb {Z}_4\), not a \(\mathbb {Z}_2\), on spin-\(\tfrac 12\).
12.2 Antiunitary conjugation is transposition
For a Hermitian matrix, entrywise complex conjugation coincides with transposition.
This is the bridge from the physics statement (time reversal is antiunitary) to the matrix statement analysed below (time reversal involves a transpose).
12.3 Transposition is positive but not completely positive
The transpose preserves positive semidefiniteness, so on its own it looks like a legal operation on states. It is not: tensoring with an untouched auxiliary system destroys positivity. Formalized here without appeal to any physics input.
\(\Phi \) is completely positive if \(\Phi \otimes \mathrm{id}_\beta \) maps positive semidefinite matrices to positive semidefinite matrices for every finite auxiliary dimension \(\beta \).
If \(\Phi \) is completely positive then its Choi matrix is positive semidefinite. Proved for an arbitrary finite-dimensional linear map, not just the transpose. Its contrapositive (GppChoiMatrix.not_completelyPositive_of_not_posSemidef_choiMatrix) is the tool used below.
An exact finite computation: the same product of Kronecker deltas on both sides.
The singlet \(\psi \) satisfies \(\mathrm{SWAP}\, \psi = -\psi \) with \(\psi \neq 0\) (GppHalfFlipMatrix.SWAP_mulVec_psi, GppHalfFlipMatrix.psi_ne_zero), giving an explicit negative eigenvector. Note this is the strong statement — not positive semidefinite in Mathlib’s own sense — rather than merely “has a negative eigenvalue”.
Proved clean, with no sorry and no axiom. Chaining the three results above: the Choi matrix of the transpose is SWAP, SWAP is not positive semidefinite, so by the Choi criterion the transpose is not completely positive.
Why this matters here. By 12.5, antiunitary time reversal carries a transpose. So the half-flip is not an artefact of a phase convention: the operation genuinely fails to be a channel, and the obstruction is the same negative eigenvector that makes the singlet antisymmetric.
12.4 Entanglement bounds (same module family)
The constructed CHSH value equals \(-1-\sqrt2\) (GppCHSHViolation.chshValue_eq), exceeds the classical bound \(2\) in modulus, and respects Tsirelson’s bound \(2\sqrt2\) (GppCHSHViolation.chshValue_within_tsirelson_bound). All three proved clean.