Equivalence of PPT-squared and IPT-squared

Abstract

The complex PPT-squared conjecture is equivalent to the IPT-squared conjectures over the complex and real fields. The reverse implications use a two-dimensional flag and preserve composition.

Definition 1.1 (Amplification).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right){\to }_{l[K]}\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),K\right),\forall r\in \mathbb{N},\forall P\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(r\right),\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(r\right),K\right),\mathrm{MatrixMap}.\mathrm{kron}\left(Phi,\mathrm{LinearMap}.\mathrm{id}:\mathrm{MatrixMap}\left(\mathrm{Fin}\left(r\right),\mathrm{Fin}\left(r\right),K\right)\right)\left(P\right)=\mathrm{fun}(a:\mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(r\right))\mapsto \mathrm{fun}(b:\mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(r\right))\mapsto Phi\left((\mathrm{fun}(i:\mathrm{Fin}\left(n\right))\mapsto \mathrm{fun}(j:\mathrm{Fin}\left(n\right))\mapsto P\left((i,a.2),(j,b.2)\right))\right)\left(a.1,b.1\right)$$

Formalization. D5/S3/Quantum/Foundation/FiniteKrausChannel.kron (✓ std3).

Citation. Giulio Chiribella; Kenneth R. Davidson; Vern I. Paulsen; Mizanur Rahaman (2023). Positive maps and entanglement in real Hilbert spaces. DOI: 10.1007/s00023-023-01325-x. URL: https://arxiv.org/abs/2207.02510v2.

Commentary.

MatrixMap.kron supplies the amplification Phi tensor the identity on Fin r; kron_id_apply gives the displayed coordinate expression. The scalar K represents the Lean parameter 𝕜 with its RCLike instance. All indices use Fin; ordered pairs put the map’s factor first. This is the coordinate encoding of Section 8, PDF p. 18.

Theorem 1.2 (Coordinates of an identity amplification).

$$\forall (\mathbb{k}:\mathrm{Type}),[\mathrm{RCLike}\left(\mathbb{k}\right)]\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{k}\right){\to }_{l[\mathbb{k}]}\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),\mathbb{k}\right),\forall r\in \mathbb{N},\forall P\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(r\right),\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(r\right),\mathbb{k}\right),\forall a\in \mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(r\right),\forall b\in \mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(r\right),\mathrm{MatrixMap}.\mathrm{kron}\left(Phi,(\mathrm{LinearMap}.\mathrm{id}:\mathrm{MatrixMap}\left(\mathrm{Fin}\left(r\right),\mathrm{Fin}\left(r\right),\mathbb{k}\right))\right)\left(P,a,b\right)=Phi\left((\mathrm{fun}(i:\mathrm{Fin}\left(n\right))\mapsto \mathrm{fun}(j:\mathrm{Fin}\left(n\right))\mapsto P\left((i,a.2),(j,b.2)\right))\right)\left(a.1,b.1\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.kron_id_apply (✓ std3). ∎

Source. Repository-derived.

Commentary.

Over every RCLike field 𝕜 and all finite input, output and ancillary dimensions, amplifying a linear matrix map Phi by the identity applies Phi to each matrix slice with the ancillary indices fixed.

Theorem 1.3 (Identity amplification on a product matrix).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right){\to }_{l[K]}\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),K\right),\forall r\in \mathbb{N},\forall A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right),\forall B\in \mathrm{Matrix}\left(\mathrm{Fin}\left(r\right),\mathrm{Fin}\left(r\right),K\right),\mathrm{MatrixMap}.\mathrm{kron}\left(Phi,\mathrm{LinearMap}.\mathrm{id}:\mathrm{MatrixMap}\left(\mathrm{Fin}\left(r\right),\mathrm{Fin}\left(r\right),K\right)\right)\left(\mathrm{Matrix}.\mathrm{kronecker}\left(A,B\right)\right)=\mathrm{Matrix}.\mathrm{kronecker}\left(Phi\left(A\right),B\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.ampl_kron (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every RCLike field and finite system and ancillary dimensions, identity amplification sends the product A tensor B to Phi(A) tensor B.

Definition 1.4 (Complete positivity).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right){\to }_{l[K]}\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),K\right),\mathrm{MatrixMap}.\mathrm{IsCompletelyPositive}\left(Phi\right)\iff (\forall r\in \mathbb{N},\forall P\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(r\right),\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(r\right),K\right),(\mathrm{Matrix}.\mathrm{PosSemidef}\left(P\right))\Rightarrow (\mathrm{Matrix}.\mathrm{PosSemidef}\left(\mathrm{MatrixMap}.\mathrm{kron}\left(Phi,\mathrm{LinearMap}.\mathrm{id}:\mathrm{MatrixMap}\left(\mathrm{Fin}\left(r\right),\mathrm{Fin}\left(r\right),K\right)\right)\left(P\right)\right)))$$

Formalization. D5/S3/Quantum/Foundation/FiniteKrausChannel.IsCompletelyPositive (✓ std3).

Citation. Giulio Chiribella; Kenneth R. Davidson; Vern I. Paulsen; Mizanur Rahaman (2023). Positive maps and entanglement in real Hilbert spaces. DOI: 10.1007/s00023-023-01325-x. URL: https://arxiv.org/abs/2207.02510v2.

Commentary.

MatrixMap.IsCompletelyPositive states that a map is completely positive when every amplification preserves positive semidefiniteness. Matrix.PosSemidef is the pinned matrix predicate. Quantification includes r = 0; that case contains only the empty matrix.

Definition 1.5 (Separable cone).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]\forall m\in \mathbb{N},\forall r\in \mathbb{N},\mathrm{SEP}\left(K,m,r\right)=\{X:\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(r\right),\mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(r\right),K\right)\mid \exists k\in \mathbb{N},\exists x\in \mathrm{Fin}\left(k\right)\to \left(\mathrm{Fin}\left(m\right)\to K\right),\exists y\in \mathrm{Fin}\left(k\right)\to \left(\mathrm{Fin}\left(r\right)\to K\right),X=\sum _{j:\mathrm{Fin}\left(k\right)}(\mathrm{Matrix}.\mathrm{kroneckerMap}\left((\mathrm{fun}(a:K)\mapsto \mathrm{fun}(b:K)\mapsto a\ast b),\mathrm{Matrix}.\mathrm{vecMulVec}\left(x\left(j\right),\mathrm{star}\left(x\left(j\right)\right)\right),\mathrm{Matrix}.\mathrm{vecMulVec}\left(y\left(j\right),\mathrm{star}\left(y\left(j\right)\right)\right)\right))\}$$

Formalization. D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.SEP (✓ std3).

Citation. Giulio Chiribella; Kenneth R. Davidson; Vern I. Paulsen; Mizanur Rahaman (2023). Positive maps and entanglement in real Hilbert spaces. DOI: 10.1007/s00023-023-01325-x. URL: https://arxiv.org/abs/2207.02510v2.

Commentary.

Section 6 defines the separable cone by finite sums of products of rank-one positive matrices. Nonnegative coefficients are absorbed into the vectors. The displayed finite sum runs over all j : Fin k. Matrix.kroneckerMap uses scalar multiplication of entries, and star acts pointwise on each vector.

Definition 1.6 (Entanglement breaking).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right){\to }_{l[K]}\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),K\right),\mathrm{IsEB}\left(Phi\right)\iff (\forall r\in \mathbb{N},\forall P\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(r\right),\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(r\right),K\right),(\mathrm{Matrix}.\mathrm{PosSemidef}\left(P\right))\Rightarrow (\mathrm{MatrixMap}.\mathrm{kron}\left(Phi,\mathrm{LinearMap}.\mathrm{id}:\mathrm{MatrixMap}\left(\mathrm{Fin}\left(r\right),\mathrm{Fin}\left(r\right),K\right)\right)\left(P\right)\in \mathrm{SEP}\left(K,m,r\right)))$$

Formalization. D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.IsEB (✓ std3).

Citation. Giulio Chiribella; Kenneth R. Davidson; Vern I. Paulsen; Mizanur Rahaman (2023). Positive maps and entanglement in real Hilbert spaces. DOI: 10.1007/s00023-023-01325-x. URL: https://arxiv.org/abs/2207.02510v2.

Commentary.

Section 8, PDF p. 18: “For p = 1, we just call the map Φ 𝕂-entanglement breaking.” Its preceding condition is (Φ ⊗ idᵣ)(P) ∈ SEPₚ(𝕂ᵐ ⊗ 𝕂ʳ) for all positive P and r ≥ 1. The display specializes p to one and adds only the vacuous empty amplification. No trace-preserving or unital condition is imposed.

Definition 1.7 (Input-first Choi matrix).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right){\to }_{l[K]}\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),K\right),\mathrm{Matrix}.\mathrm{submatrix}\left((\mathrm{fun}(j:\mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(n\right))\mapsto \mathrm{fun}(k:\mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(n\right))\mapsto Phi\left(\mathrm{Matrix}.\mathrm{single}\left(j.2,k.2,1\right)\right)\left(j.1,k.1\right)),\mathrm{Prod}.\mathrm{swap},\mathrm{Prod}.\mathrm{swap}\right)=\mathrm{fun}(a:\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(m\right))\mapsto \mathrm{fun}(b:\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(m\right))\mapsto Phi\left(\mathrm{Matrix}.\mathrm{single}\left(a.1,b.1,1\right)\right)\left(a.2,b.2\right)$$

Formalization. D5/S3/Quantum/Foundation/FiniteKrausRepresentation.choi_matrix (✓ std3).

Citation. Giulio Chiribella; Kenneth R. Davidson; Vern I. Paulsen; Mizanur Rahaman (2023). Positive maps and entanglement in real Hilbert spaces. DOI: 10.1007/s00023-023-01325-x. URL: https://arxiv.org/abs/2207.02510v2.

Commentary.

MatrixMap.choi_matrix supplies the displayed output-first coordinate expression; submatrix Prod.swap Prod.swap puts the input factor first. Applying Phi to the matrix unit Matrix.single a.1 b.1 1 gives its entry at output indices a.2 and b.2. The canonical Kraus Choi matrix places output first; Prod.swap relates the two tensor orders.

Theorem 1.8 (Complete positivity gives Choi positivity).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right){\to }_{l[K]}\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),K\right),(\mathrm{MatrixMap}.\mathrm{IsCompletelyPositive}\left(Phi\right))\Rightarrow (\mathrm{Matrix}.\mathrm{PosSemidef}\left(\mathrm{Matrix}.\mathrm{submatrix}\left((\mathrm{fun}(j:\mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(n\right))\mapsto \mathrm{fun}(k:\mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(n\right))\mapsto Phi\left(\mathrm{Matrix}.\mathrm{single}\left(j.2,k.2,1\right)\right)\left(j.1,k.1\right)),\mathrm{Prod}.\mathrm{swap},\mathrm{Prod}.\mathrm{swap}\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.choi_psd_of_cp (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every RCLike scalar field K and all natural dimensions n and m, a completely positive K-linear map Phi from n by n matrices to m by m matrices has a positive semidefinite input-first Choi matrix. The input-first matrix is MatrixMap.choi_matrix Phi with both indices composed with Prod.swap. The IPT-to-PPT implication uses this positivity, and swapping the tensor factors again gives the output-first positivity used for qubit channels.

Definition 1.9 (Partial transpose on the first factor).

$$\forall K\in \mathrm{Type},\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall X\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(m\right),K\right),\mathrm{ptFirst}\left(X\right)=\mathrm{fun}(a:\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(m\right))\mapsto \mathrm{fun}(b:\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(m\right))\mapsto X\left((b.1,a.2),(a.1,b.2)\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.ptFirst (✓ std3).

Citation. Giulio Chiribella; Kenneth R. Davidson; Vern I. Paulsen; Mizanur Rahaman (2023). Positive maps and entanglement in real Hilbert spaces. DOI: 10.1007/s00023-023-01325-x. URL: https://arxiv.org/abs/2207.02510v2.

Commentary.

The first coordinates are exchanged and the second coordinates retained. This is τₙ tensor idₘ in Section 9.1, PDF p. 21; it is an ordinary transpose without complex conjugation.

Definition 1.10 (PPT maps).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right){\to }_{l[K]}\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),K\right),\mathrm{IsPPT}\left(Phi\right)\iff ((\mathrm{MatrixMap}.\mathrm{IsCompletelyPositive}\left(Phi\right))\wedge (\mathrm{Matrix}.\mathrm{PosSemidef}\left(\mathrm{ptFirst}\left(\mathrm{Matrix}.\mathrm{submatrix}\left((\mathrm{fun}(j:\mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(n\right))\mapsto \mathrm{fun}(k:\mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(n\right))\mapsto Phi\left(\mathrm{Matrix}.\mathrm{single}\left(j.2,k.2,1\right)\right)\left(j.1,k.1\right)),\mathrm{Prod}.\mathrm{swap},\mathrm{Prod}.\mathrm{swap}\right)\right)\right)))$$

Formalization. D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.IsPPT (✓ std3).

Citation. Giulio Chiribella; Kenneth R. Davidson; Vern I. Paulsen; Mizanur Rahaman (2023). Positive maps and entanglement in real Hilbert spaces. DOI: 10.1007/s00023-023-01325-x. URL: https://arxiv.org/abs/2207.02510v2.

Commentary.

Section 9.1, PDF p. 21: “A completely positive map Φ : Mₙ(𝕂) → Mₘ(𝕂) is called PPT (IPT) if its Choi matrix is PPT (IPT).” Here PPT requires the first-factor partial transpose of the Choi matrix to be positive semidefinite.

Definition 1.11 (IPT maps).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right){\to }_{l[K]}\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),K\right),\mathrm{IsIPT}\left(Phi\right)\iff ((\mathrm{MatrixMap}.\mathrm{IsCompletelyPositive}\left(Phi\right))\wedge (\mathrm{ptFirst}\left(\mathrm{Matrix}.\mathrm{submatrix}\left((\mathrm{fun}(j:\mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(n\right))\mapsto \mathrm{fun}(k:\mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(n\right))\mapsto Phi\left(\mathrm{Matrix}.\mathrm{single}\left(j.2,k.2,1\right)\right)\left(j.1,k.1\right)),\mathrm{Prod}.\mathrm{swap},\mathrm{Prod}.\mathrm{swap}\right)\right)=\mathrm{Matrix}.\mathrm{submatrix}\left((\mathrm{fun}(j:\mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(n\right))\mapsto \mathrm{fun}(k:\mathrm{Fin}\left(m\right)\times \mathrm{Fin}\left(n\right))\mapsto Phi\left(\mathrm{Matrix}.\mathrm{single}\left(j.2,k.2,1\right)\right)\left(j.1,k.1\right)),\mathrm{Prod}.\mathrm{swap},\mathrm{Prod}.\mathrm{swap}\right)))$$

Formalization. D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.IsIPT (✓ std3).

Citation. Giulio Chiribella; Kenneth R. Davidson; Vern I. Paulsen; Mizanur Rahaman (2023). Positive maps and entanglement in real Hilbert spaces. DOI: 10.1007/s00023-023-01325-x. URL: https://arxiv.org/abs/2207.02510v2.

Commentary.

Section 9.1, PDF p. 21: “A completely positive map Φ : Mₙ(𝕂) → Mₘ(𝕂) is called PPT (IPT) if its Choi matrix is PPT (IPT).” Here IPT requires equality of the Choi matrix with its first-factor partial transpose.

Definition 1.12 (The complex PPT-squared conjecture).

$$PPT2C\iff (\forall n\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right){\to }_{l[\mathbb{C}]}\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),(\mathrm{IsPPT}\left(Phi\right))\Rightarrow (\mathrm{IsEB}\left((Phi{\circ }_{l}Phi)\right)))$$

Formalization. D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.PPT2C (✓ std3).

Citation. Giulio Chiribella; Kenneth R. Davidson; Vern I. Paulsen; Mizanur Rahaman (2023). Positive maps and entanglement in real Hilbert spaces. DOI: 10.1007/s00023-023-01325-x. URL: https://arxiv.org/abs/2207.02510v2.

Commentary.

Conjecture 9.5, PDF p. 23: “For every PPT map Φ : Mₙ(ℂ) → Mₙ(ℂ), Φ ◦ Φ is ℂ-entanglement breaking.” The dimension n is universally quantified. The linear-map composition Phi ∘ₗ Phi is the square.

Definition 1.13 (The IPT-squared conjecture).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]IPT2\left(K\right)\iff (\forall n\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right){\to }_{l[K]}\mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right),(\mathrm{IsIPT}\left(Phi\right))\Rightarrow (\mathrm{IsEB}\left((Phi{\circ }_{l}Phi)\right)))$$

Formalization. D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.IPT2 (✓ std3).

Citation. Giulio Chiribella; Kenneth R. Davidson; Vern I. Paulsen; Mizanur Rahaman (2023). Positive maps and entanglement in real Hilbert spaces. DOI: 10.1007/s00023-023-01325-x. URL: https://arxiv.org/abs/2207.02510v2.

Commentary.

Conjecture 9.7, PDF p. 24: “For 𝕂 ∈ {ℝ, ℂ}, every IPT map Φ : Mₙ(𝕂) → Mₙ(𝕂) satisfies Φ ◦ Φ is 𝕂-entanglement breaking.” The definition is generic over RCLike K and is used at ℝ and ℂ. Zero dimension adds only a vacuous case.

Definition 1.14 (The equivalence question).

$$claim\iff ((PPT2C\iff (IPT2\left(\mathbb{C}\right)))\wedge (IPT2\left(\mathbb{C}\right)\iff (IPT2\left(\mathbb{R}\right))))$$

Formalization. D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.claim (✓ std3).

Citation. Giulio Chiribella; Kenneth R. Davidson; Vern I. Paulsen; Mizanur Rahaman (2023). Positive maps and entanglement in real Hilbert spaces. DOI: 10.1007/s00023-023-01325-x. URL: https://arxiv.org/abs/2207.02510v2.

Commentary.

Section 9.2, after Proposition 9.9, PDF p. 25: “We do not know if these conjectures are equivalent.” The encoding is the conjunction (PPT2C ↔ IPT2 ℂ) ∧ (IPT2 ℂ ↔ IPT2 ℝ). Each conjecture ranges over all dimensions; this does not assert that the conjectures themselves are true.

Remark 1.15 (A composition-compatible flag).

$$\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(m\right)),(\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(m\right)),\mathbb{C}\right),\forall Pplus\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\forall Pminus\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),((Pplus=\frac{((1,\mathrm{Complex}.I)((1,\mathrm{Complex}.I){)}^{\ast })}{2})\wedge (Pminus=\frac{((1,-\mathrm{Complex}.I)((1,-\mathrm{Complex}.I){)}^{\ast })}{2}))\Rightarrow (((\mathrm{Matrix}.\mathrm{PosSemidef}\left(rho\right))\wedge (\mathrm{Matrix}.\mathrm{PosSemidef}\left(((rho{)}^{{\Gamma }_B})\right)))\Rightarrow (\exists rhotilde\in \mathrm{Matrix}\left(((\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(m\right))\times \mathrm{Fin}\left(2\right)),((\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(m\right))\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(rhotilde=((\mathrm{Matrix}.\mathrm{kroneckerMap}\left((\mathrm{fun}(a:\mathbb{C})\mapsto \mathrm{fun}(b:\mathbb{C})\mapsto a\ast b),rho,Pplus\right))+(\mathrm{Matrix}.\mathrm{kroneckerMap}\left((\mathrm{fun}(a:\mathbb{C})\mapsto \mathrm{fun}(b:\mathbb{C})\mapsto a\ast b),((rho{)}^{{\Gamma }_B}),Pminus\right))))\wedge ((\mathrm{Matrix}.\mathrm{PosSemidef}\left(rhotilde\right))\wedge ((rhotilde{)}^{{\Gamma }_{B{B}^{\prime }}}=rhotilde))))$$

Citation. Marcus Huber; Ludovico Lami; Cécilia Lancien; Alexander Müller-Hermes (2018). High-Dimensional Entanglement in States with Positive Partial Transposition. DOI: 10.1103/PhysRevLett.121.200503. URL: https://arxiv.org/abs/1802.04975.

Commentary.

On the auxiliary two-dimensional factor take P+ = (1,i)(1,i)/2 and P- = (1,-i)(1,-i)/2. Their transpose exchanges them. Compress to these flag sectors with B+ and B-, and put E(X) = B+(X) + B-(X)^T and D(A) = A tensor P+ + A^T tensor P-. The lift D Phi E/2 has four completely positive branches for every complex PPT Phi. It is invariant under transpose on input and output, so its real restriction is IPT and complexifies back to the lift. The identity E D = 2 id makes the lift preserve composition. Completely positive insertion A tensor P+ and compression B+ recover Phi squared divided by two. This transfers entanglement breaking from the lifted square. The lift adapts the conjugate-flag construction rho tensor P+ + rho partially transposed tensor P- of Huber, Lami, Lancien and Müller-Hermes, arXiv v1, Section III.C, PDF p. 8, the second lemma labelled III.1. The map normalization, composition law and recovery are the consequences used here.

Definition 1.16 (Normalized finite separable mixtures).

$$\forall X\in \mathrm{Type},[\mathrm{Fintype}\left(X\right)]\forall Y\in \mathrm{Type},[\mathrm{Fintype}\left(Y\right)]\forall rho\in \mathrm{Matrix}\left(X\times Y,X\times Y,\mathbb{C}\right),\mathrm{IsSeparable}\left(rho\right)\iff (\exists n\in \mathbb{N},\exists p\in \mathrm{Fin}\left(n\right)\to \mathbb{R},\exists sigma\in \mathrm{Fin}\left(n\right)\to \mathrm{Matrix}\left(X,X,\mathbb{C}\right),\exists tau\in \mathrm{Fin}\left(n\right)\to \mathrm{Matrix}\left(Y,Y,\mathbb{C}\right),(\forall i\in \mathrm{Fin}\left(n\right),0\le p\left(i\right))\wedge ((\sum _{i:\mathrm{Fin}\left(n\right)}(p\left(i\right))=1)\wedge ((\forall i\in \mathrm{Fin}\left(n\right),((\mathrm{Matrix}.\mathrm{PosSemidef}\left(sigma\left(i\right)\right))\wedge (\mathrm{Matrix}.\mathrm{trace}\left(sigma\left(i\right)\right)=1))\wedge ((\mathrm{Matrix}.\mathrm{PosSemidef}\left(tau\left(i\right)\right))\wedge (\mathrm{Matrix}.\mathrm{trace}\left(tau\left(i\right)\right)=1)))\wedge (rho=\sum _{i:\mathrm{Fin}\left(n\right)}(\mathrm{HSMul}.\mathrm{hSMul}\left((p\left(i\right):\mathbb{C}),\mathrm{Matrix}.\mathrm{kronecker}\left(sigma\left(i\right),tau\left(i\right)\right)\right))))))$$

Formalization. D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.IsSeparable (✓ std3).

Source. Repository-derived.

Commentary.

A separable bipartite matrix is a finite convex mixture of tensor products of positive semidefinite trace-one matrices. The two index types are arbitrary finite types.

Definition 1.17 (The conditional ancillary matrix).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]\forall n\in \mathbb{N},\forall r\in \mathbb{N},\forall M\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right),\forall P\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(r\right),\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(r\right),K\right),\mathrm{weighted}\left(M,P\right)=\mathrm{fun}(u:\mathrm{Fin}\left(r\right))\mapsto \mathrm{fun}(v:\mathrm{Fin}\left(r\right))\mapsto \mathrm{Matrix}.\mathrm{trace}\left((M\ast (\mathrm{fun}(i:\mathrm{Fin}\left(n\right))\mapsto \mathrm{fun}(j:\mathrm{Fin}\left(n\right))\mapsto P\left((i,u),(j,v)\right)))\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.weighted (✓ std3).

Source. Repository-derived.

Commentary.

The effect M is paired by trace with each system slice of P; the remaining two coordinates index the ancillary matrix.

Theorem 1.18 (Positive conditional ancillary matrices).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]\forall n\in \mathbb{N},\forall r\in \mathbb{N},\forall M\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right),\forall P\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(r\right),\mathrm{Fin}\left(n\right)\times \mathrm{Fin}\left(r\right),K\right),(\mathrm{Matrix}.\mathrm{PosSemidef}\left(M\right))\Rightarrow ((\mathrm{Matrix}.\mathrm{PosSemidef}\left(P\right))\Rightarrow (\mathrm{Matrix}.\mathrm{PosSemidef}\left(\mathrm{weighted}\left(M,P\right)\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.weighted_psd (✓ std3). ∎

Source. Repository-derived.

Commentary.

A positive effect and a positive joint input give a positive conditional ancillary matrix, by rank-one decomposition and positive congruence.

Definition 1.19 (Finite positive measure-and-prepare form).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right){\to }_{l[K]}\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),K\right),\mathrm{HasPrepare}\left(Phi\right)\iff (\exists k\in \mathbb{N},\exists M\in \mathrm{Fin}\left(k\right)\to \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right),\exists N\in \mathrm{Fin}\left(k\right)\to \mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),K\right),(\forall j\in \mathrm{Fin}\left(k\right),(\mathrm{Matrix}.\mathrm{PosSemidef}\left(M\left(j\right)\right))\wedge (\mathrm{Matrix}.\mathrm{PosSemidef}\left(N\left(j\right)\right)))\wedge (\forall A\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right),Phi\left(A\right)=\sum _{j:\mathrm{Fin}\left(k\right)}(\mathrm{Matrix}.\mathrm{trace}\left((M\left(j\right)\ast A)\right)\cdot N\left(j\right))))$$

Formalization. D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.HasPrepare (✓ std3).

Source. Repository-derived.

Commentary.

A finite family of positive measurement matrices M and positive preparation matrices N represents Phi by the sum of trace(M(j) A) times N(j), for every input matrix A. The natural number k counts all terms; n and m are arbitrary input and output dimensions over an RCLike scalar field K. Scalar multiplication is displayed by a centered dot.

Theorem 1.20 (Positive measure-and-prepare maps break entanglement).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right){\to }_{l[K]}\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),K\right),(\mathrm{HasPrepare}\left(Phi\right))\Rightarrow (\mathrm{IsEB}\left(Phi\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.prepare_eb (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every positive amplified input has separable output under a map with finite positive measure-and-prepare form. Positivity of each weighted matrix follows from a rank-one decomposition of the measurement matrix and positive congruence of the input; tensor products with the positive preparations then form a finite separable sum.

Theorem 1.21 (Composition preserves complete positivity).

$$\forall K\in \mathrm{Type},[\mathrm{RCLike}\left(K\right)]\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall p\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),K\right){\to }_{l[K]}\mathrm{Matrix}\left(\mathrm{Fin}\left(p\right),\mathrm{Fin}\left(p\right),K\right),\forall Psi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),K\right){\to }_{l[K]}\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),K\right),(\mathrm{MatrixMap}.\mathrm{IsCompletelyPositive}\left(Phi\right))\Rightarrow ((\mathrm{MatrixMap}.\mathrm{IsCompletelyPositive}\left(Psi\right))\Rightarrow (\mathrm{MatrixMap}.\mathrm{IsCompletelyPositive}\left((Phi){\circ }_l(Psi)\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.cp_comp (✓ std3). ∎

Source. Repository-derived.

Commentary.

The composition of completely positive linear matrix maps is completely positive, over every RCLike field and all finite dimensions.

Theorem 1.22 (Double transposition preserves complete positivity).

$$\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right){\to }_{l[\mathbb{C}]}\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),\mathbb{C}\right),(\mathrm{MatrixMap}.\mathrm{IsCompletelyPositive}\left(Phi\right))\Rightarrow (\mathrm{MatrixMap}.\mathrm{IsCompletelyPositive}\left((\mathrm{LinearEquiv}.\mathrm{toLinearMap}\left(\mathrm{Matrix}.\mathrm{transposeLinearEquiv}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),\mathbb{C},\mathbb{C}\right)\right)){\circ }_l((Phi){\circ }_l(\mathrm{LinearEquiv}.\mathrm{toLinearMap}\left(\mathrm{Matrix}.\mathrm{transposeLinearEquiv}\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(n\right),\mathbb{C},\mathbb{C}\right)\right)))\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.cp_double_tau (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every completely positive complex-linear matrix map, transposing its input and output gives a completely positive map. Input and output dimensions may differ.

Theorem 1.23 (The three conjectures are equivalent).

$$(PPT2C\iff (IPT2\left(\mathbb{C}\right)))\wedge (IPT2\left(\mathbb{C}\right)\iff (IPT2\left(\mathbb{R}\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.result (✓ std3). ∎

Resolves. Problems/chiribella-davidson-paulsen-rahaman-2023-ppt-ipt-squared-equivalence (proved) by D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.result.

Source. Repository-derived.

Acknowledgement. Giulio Chiribella; Kenneth R. Davidson; Vern I. Paulsen; Mizanur Rahaman (2023). Positive maps and entanglement in real Hilbert spaces. DOI: 10.1007/s00023-023-01325-x. URL: https://arxiv.org/abs/2207.02510v2.

Commentary.

IPT² over either field in dimension 2n implies PPT² over ℂ in dimension n by the flag lift and recovery. The source’s implications PPT²(ℂ) ⇒ IPT²(ℂ) ⇒ IPT²(ℝ) retain dimension n. Entanglement breaking is characterized by a separable input-first Choi matrix, with an explicit tensor swap, and by measure-and-prepare form. Completely positive maps preserve it under pre- and post-composition. The complexification of a real entanglement-breaking map is complex entanglement breaking; in the reverse direction the IPT condition gives CSEP ∩ IPT = real SEP. These facts close both equivalences. The PPT-squared conjecture itself and the possibility of avoiding dimension doubling remain open.

References

• Truth anchor: D5/S3/Quantum/Foundation/FiniteKrausChannel.IsCompletelyPositive
• Truth anchor: D5/S3/Quantum/Foundation/FiniteKrausChannel.kron
• Truth anchor: D5/S3/Quantum/Foundation/FiniteKrausRepresentation.choi_matrix
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.HasPrepare
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.IPT2
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.IsEB
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.IsIPT
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.IsPPT
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.IsSeparable
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.PPT2C
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.SEP
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.ampl_kron
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.choi_psd_of_cp
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.claim
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.cp_comp
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.cp_double_tau
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.kron_id_apply
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.prepare_eb
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.ptFirst
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.result
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.weighted
• Truth anchor: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence.weighted_psd
• Dependency: D5/S3/Quantum/Foundation/FiniteKrausRepresentation
• Dependency: D5/S3/Weil/Probability/FiniteGaussianSchoenberg