# Entanglement without distillable secret key

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

- [Entanglement with zero distillable secret key in local dimension ten](../../preprints/Entanglement-with-zero-distillable-secret-key-in-local-dimension-ten-September-27-2026/paper.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| PPT channel on dimension 21 whose square is not entanglement breaking | [DimensionTenChannel.lean](../ComparatorChallenges/DimensionTenChannel.lean) |
| Dimension-ten PPT pair with non-entanglement-breaking composition | [DimensionTenPair.lean](../ComparatorChallenges/DimensionTenPair.lean) |