Compatibility need not imply Jordan compatibility
Abstract
Two compatible channels on four-dimensional complex matrices need not be Jordan compatible.
Definition 1.1 (Complex square matrices).
Formalization. D5/S3/QuantumChannels/JordanCompatibilityRefutation.Mat (✓ std3).
Source. Repository-derived.
Commentary.
For an index type of any universe, Mat is the type of complex square matrices on that type.
Definition 1.2 (Complex linear maps between matrix spaces).
Formalization. D5/S3/QuantumChannels/JordanCompatibilityRefutation.Map (✓ std3).
Source. Repository-derived.
Commentary.
Map is the MatrixMap abbreviation for complex linear maps between the two square-matrix spaces. Both index types may belong to arbitrary universes.
Matrix conventions
The tensor index is Fin d × (Fin d × Fin d), with the reference coordinate first. Fin d includes every natural d, including zero. Products below retain this association. A centered dot denotes matrix multiplication for matrix operands and complex multiplication for scalar operands. Matrix.conjTranspose is conjugate transpose.
Matrix.IsHermitian means equality with the conjugate transpose. Matrix.PosSemidef includes Hermitian symmetry and nonnegativity of the quadratic form on every finitely supported complex vector. The inequality uses the complex order.
The channel predicate is finite Kraus form with identity normalization. The input and output index types are finite with decidable equality; no condition on an individual input matrix is imposed. Bracketed Fintype and DecidableEq assumptions are anonymous typeclass assumptions.
The two partial traces of a joint output sum over its first and second coordinates, respectively.
LinearMap.id acts as the identity on every input matrix. MatrixMap.kron acts on matrix units by the following finite sum, with both maps complex linear. The displayed specializations have the same input and output index type in each factor. Bracketed Fintype and DecidableEq assumptions are anonymous typeclass assumptions.
MatrixMap.choi_matrix uses output-first indices. For LinearMap.id its entries are those of the matrix unit with the second pair of coordinates as labels. This is the operator in equation (117), equivalently equation (120).
Definition 1.3 (Tracing out the middle input factor).
Formalization. D5/S3/QuantumChannels/JordanCompatibilityRefutation.traceX1 (✓ std3).
Citation. Mark Girard; Martin Plávala; Jamie Sikora (2021). Jordan products of quantum channels and their compatibility. DOI: 10.1038/s41467-021-22275-0. URL: https://arxiv.org/abs/2009.03279v1.
Commentary.
Definition 25, equation (117): traceX1 sums the middle coordinate of the three-factor matrix and retains the reference and last coordinates.
Definition 1.4 (Tracing out the last input factor).
Formalization. D5/S3/QuantumChannels/JordanCompatibilityRefutation.traceX2 (✓ std3).
Citation. Mark Girard; Martin Plávala; Jamie Sikora (2021). Jordan products of quantum channels and their compatibility. DOI: 10.1038/s41467-021-22275-0. URL: https://arxiv.org/abs/2009.03279v1.
Commentary.
Definition 25, equation (117): traceX2 sums the last coordinate and retains the reference and middle coordinates.
Definition 1.5 (The Choi matrix of the generalized Jordan product).
Formalization. D5/S3/QuantumChannels/JordanCompatibilityRefutation.jordanAction (✓ std3).
Citation. Mark Girard; Martin Plávala; Jamie Sikora (2021). Jordan products of quantum channels and their compatibility. DOI: 10.1038/s41467-021-22275-0. URL: https://arxiv.org/abs/2009.03279v1.
Commentary.
Definition 25, equation (119): apply the identity to the reference factor and the two maps to the other factors. This operation is defined on every matrix A; Hermitian symmetry and the two marginal equations enter JordanCompatible separately.
Definition 1.6 (A joint channel with the prescribed marginals).
Formalization. D5/S3/QuantumChannels/JordanCompatibilityRefutation.Compatible (✓ std3).
Citation. Mark Girard; Martin Plávala; Jamie Sikora (2021). Jordan products of quantum channels and their compatibility. DOI: 10.1038/s41467-021-22275-0. URL: https://arxiv.org/abs/2009.03279v1.
Commentary.
Compatibility means that a channel into the product output space has the two prescribed partial traces on every complex input matrix. The predicate itself requires the joint map to be a channel; the channel assumptions on the two given maps are explicit in claim.
Definition 1.7 (A Hermitian operator with positive Jordan image).
Formalization. D5/S3/QuantumChannels/JordanCompatibilityRefutation.JordanCompatible (✓ std3).
Citation. Mark Girard; Martin Plávala; Jamie Sikora (2021). Jordan products of quantum channels and their compatibility. DOI: 10.1038/s41467-021-22275-0. URL: https://arxiv.org/abs/2009.03279v1.
Commentary.
Definition 27 requires a Hermitian A satisfying both equations (117), whose generalized Jordan product is completely positive. By the Choi criterion this is positive semidefiniteness of jordanAction. A itself need not be positive semidefinite. Proposition 26 gives compatibility from these conditions for channels.
Definition 1.8 (The conjecture following Theorem 30).
Formalization. D5/S3/QuantumChannels/JordanCompatibilityRefutation.claim (✓ std3).
Citation. Mark Girard; Martin Plávala; Jamie Sikora (2021). Jordan products of quantum channels and their compatibility. DOI: 10.1038/s41467-021-22275-0. URL: https://arxiv.org/abs/2009.03279v1.
Commentary.
For every natural dimension and every pair of channels on that matrix space, compatibility implies Jordan compatibility. Theorem 30 proves this implication when both channels have inverse linear maps. The conjecture after its proof removes that invertibility hypothesis; claim states precisely this unrestricted implication.
Theorem 1.9 (A compatible pair in dimension four).
Proof. Machine-checked in Lean as D5/S3/QuantumChannels/JordanCompatibilityRefutation.result (✓ std3). ∎
Resolves. Problems/girard-plavala-sikora-2021-jordan-compatibility-refutation (refuted) by D5/S3/QuantumChannels/JordanCompatibilityRefutation.result.
Source. Repository-derived.
Acknowledgement. Mark Girard; Martin Plávala; Jamie Sikora (2021). Jordan products of quantum channels and their compatibility. DOI: 10.1038/s41467-021-22275-0. URL: https://arxiv.org/abs/2009.03279v1.
Commentary.
Let P interchange the first and third standard basis vectors and the second and fourth, and let Q = diag(1,1,−1,−1). Both are real symmetric involutions and PQ + QP = 0. Put (S₁,S₂,S₃,S₄) = (P,−P,Q,−Q), Eᵢ = (5I + 4Sᵢ)/20 and Fⱼ = (4I + 3Sⱼ)/16. These positive semidefinite effects each sum to I. The two channels send R to diag(tr(EᵢR)) and diag(tr(FⱼR)). The joint channel sends R to the diagonal matrix with entries hᵢⱼ tr(EᵢR), where hᵢⱼ = 1/64 + (15/16)δᵢⱼ and δᵢⱼ is one when i = j and zero otherwise. Its two partial traces are the two channels.
Suppose A satisfies the two marginal equations and its Jordan image is positive semidefinite. The diagonal output blocks are positive semidefinite matrices. Multiply the four blocks with first output in {1,2} and second output in {3,4} by four, and label them Gₛₜ for s,t in {1,−1}. Their total is I, their s-weighted sum is (4/5)P, and their t-weighted sum is (3/4)Q. For Hₛₜ = (3/2)I − sP − tQ, the identity Hₛₜ = (1/4)(2I − sP − tQ)†(2I − sP − tQ) makes every Hₛₜ positive semidefinite. Consequently the sum of the real parts of tr(HₛₜGₛₜ) is at least zero. The three moment identities make the same sum equal to 6 − 16/5 − 3 = −1/5, a contradiction. Thus these compatible channels are not Jordan compatible.
References
- Truth anchor:
D5/S3/QuantumChannels/JordanCompatibilityRefutation.Compatible - Truth anchor:
D5/S3/QuantumChannels/JordanCompatibilityRefutation.JordanCompatible - Truth anchor:
D5/S3/QuantumChannels/JordanCompatibilityRefutation.Map - Truth anchor:
D5/S3/QuantumChannels/JordanCompatibilityRefutation.Mat - Truth anchor:
D5/S3/QuantumChannels/JordanCompatibilityRefutation.claim - Truth anchor:
D5/S3/QuantumChannels/JordanCompatibilityRefutation.jordanAction - Truth anchor:
D5/S3/QuantumChannels/JordanCompatibilityRefutation.result - Truth anchor:
D5/S3/QuantumChannels/JordanCompatibilityRefutation.traceX1 - Truth anchor:
D5/S3/QuantumChannels/JordanCompatibilityRefutation.traceX2 - Dependency: D5/S3/Quantum/Foundation/FiniteKrausRepresentation
- Dependency: D5/S3/Quantum/Information/PartialTraceMutualInformation
- Dependency: D5/S3/Quantum/QuantumChannels/PureProgramQubitObstruction
- Dependency: D5/S3/Quantum/Recovery/KrausCompletion
- Dependency: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo