The composite Choi matrix is nonzero
ProvedOAI.DimensionTen.compositeChoi_ne_zerochoi-matrixquantum-information
The Choi matrix of the composition of the two explicit maps of the dimension-ten pair, a matrix whose entry is , is not the zero matrix. Concretely its top-left entry equals , because and then returns in that entry.
Preamble
import Mathlib import Definitions.Def_DimensionTenPair open Matrix Complex open scoped Matrix ComplexOrder
Formal statement
namespace OAI.DimensionTen theorem compositeChoi_ne_zero : choi (phiTwo ∘ phiOne) ≠ 0 := by sorry end OAI.DimensionTen
Source
OpenAI, Entanglement with zero distillable secret key in local dimension ten (September 27, 2026), https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Entanglement-with-zero-distillable-secret-key-in-local-dimension-ten-September-27-2026/paper.pdf, Section 6, proof of Proposition 6.1 (the positive definite output of L makes Z nonzero) and Section 7, equation (7.1).