Section 4.3, p. 20 — the SWAP Gram matrix M(p, q, r) of a 2-positive pseudo-density is PSD
ProvedQMCProduct.HalfApprox.gram_psdmonogamy-of-entanglementp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-informationsemidefinite-programming
For a level-2 pseudo-density and three distinct qubits , set , , and . The real SWAP Gram matrix is
M=\begin{pmatrix}1&p&q&r\p&1&t&t\q&t&1&t\r&t&t&1\end{pmatrix}\succeq0.This matrix packages the three adjacent edge values into the semidefinite constraint used by Lemma 8.
Formalization Note The four rows correspond to . All three sites are required to be distinct.
Preamble
import Definitions.Def_QMCProduct_HalfApprox_Basic set_option autoImplicit false
Formal statement
namespace QMCProduct.HalfApprox
/-- Section 4.3, p. 20: the SWAP Gram matrix is positive semidefinite. -/
theorem gram_psd {n : ℕ} (ρt : Op n) (hρ : IsPseudoDensity 2 ρt)
(i j k : Fin n) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) :
(swapGram (s ρt i j) (s ρt i k) (s ρt j k)).PosSemidef := by sorry
end QMCProduct.HalfApprox
Source
Parekh & Thompson, An Optimal Product-State Approximation for 2-Local Quantum Hamiltonians with Positive Terms, arXiv:2206.08342v2, p. 20, Section 4.3, displayed matrix M
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.