∑math20

Mathematical physics · Result 272

Entanglement without distillable secret key

1 paperLean

Constructs an entangled state on \(\mathbb C^{10}\otimes\mathbb C^{10}\) with zero distillable secret key for the specified local-instrument protocols that complete almost surely. These allow joint local processing and authenticated two-way public communication, with no other shared private resource and an eavesdropper holding the input purification and public record. A trace-preserving PPT channel on \(M_{21}(\mathbb C)\) whose square is not entanglement breaking disproves Christandl's PPT-square conjecture.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Entanglement with zero distillable secret key in local dimension ten

Entanglement with zero distillable secret key in local dimension ten

OpenAI · September 27, 2026

We construct an entangled state on \(\mathbb C^{10}\otimes\mathbb C^{10}\) with zero distillable secret key for the local-instrument protocols specified here. They allow joint processing of all copies and unlimited two-way public communication, with the input as the only shared private resource and an eavesdropper holding a purification and the complete public record. The construction also disproves the unrestricted two-map PPT-composition conjecture. A separate trace-preserving PPT channel on \(M_{21}(\mathbb C)\) has a square that is not entanglement breaking.

Read PDF Download Source

Cite
@misc{OAI:Entanglement-with-zero-distillable-secret-key-in-local-dimension-ten-September-27-2026,
  author = {{OpenAI}},
  title = {{Entanglement with zero distillable secret key in local dimension ten}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Entanglement-with-zero-distillable-secret-key-in-local-dimension-ten-September-27-2026/paper.pdf}{OAI:Entanglement-with-zero-distillable-secret-key-in-local-dimension-ten-September-27-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The paper's entanglement construction yields counterexamples to PPT-composition claims. The linked formalization covers these consequences: two explicitly specified PPT maps on \(10\times10\) complex matrices have a composition that is not entanglement breaking, and the nonzero Choi matrix of that composition has no nonzero product vector in its range. A separate trace-preserving PPT channel on \(21\times21\) matrices has a square that is not entanglement breaking.

The paper's zero-distillable-secret-key statement is outside these two selected Comparator statements.

Comparator links

ResultComparator statement
PPT channel on dimension 21 whose square is not entanglement breakingDimensionTenChannel.lean
Dimension-ten PPT pair with non-entanglement-breaking compositionDimensionTenPair.lean

Scope note on GitHub →