Fact 1: contraction sandwich identity

Proved

QAlgorithms.Papers.Independent.Extend50.P18.contraction_sandwich

by Gohan · Oct 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $d\ge1$ , $k\ge1$ , and $n=r+2k$ with $r\ge0$ . Let $V^{(k)}$ be the product of the $k$ swaps between registers $n-2k+j$ and $n-j+1$ , partially transposed on the final registers. Thus each transposed swap equals $dP^+$ for the normalized Bell projector. For every complex operator $X$ on the first $n-k$ registers,

V^{(k)}(X\otimes I_k)V^{(k)}=(\operatorname{Tr}_{n-2k+1,\ldots,n-k}X\otimes I_{2k})V^{(k)}.

The partial trace is unnormalized. The identity applies to arbitrary operators, including non-Hermitian ones, and is the contraction rule used in subsequent trace calculations.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Extend50_P18

Formal statement

noncomputable section

open scoped BigOperators Matrix ComplexOrder

namespace QAlgorithms.Papers.Independent.Extend50.P18

attribute [local instance] Classical.propDecidable

/-- Fact 1, with n=r+2k: the contraction sandwich identity for every complex
operator X, without positivity or state normalization (PDF pp.9-11, (38)). -/
theorem contraction_sandwich (d r k : ℕ) (hd : 0 < d) (hk : 0 < k)
    (X : Matrix ((Fin r → Fin d) × (Fin k → Fin d)) ((Fin r → Fin d) × (Fin k → Fin d)) ℂ) :
    pairedContraction d r k * liftInput X * pairedContraction d r k =
      liftSurvivor (k := k) (QAlgorithms.traceRight X) * pairedContraction d r k := by sorry

end QAlgorithms.Papers.Independent.Extend50.P18

end

Source

Efficient multi port-based teleportation schemes, arXiv:2008.00984v4, PDF p. 9, Fact 1

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every $d,r,k\in\mathbb N$ with $d>0$ and $k>0$ , and every complex matrix $X$ indexed by pairs $(u,v)$ , where $u:[r]\to[d]$ , $v:[k]\to[d]$ , and $[m]=\{0,\ldots,m-1\}$ , define matrices on triples $(u,(v,w))$ as follows: $C((u,(v,w)),(u',(v',w')))$ is $1$ exactly when $u=u'$ , $v(l)=w(k-1-l)$ , and $v'(l)=w'(k-1-l)$ for every $l\in[k]$ , and is zero otherwise; $L_X((u,(v,w)),(u',(v',w')))=X((u,v),(u',v'))$ when $w=w'$ , and is zero otherwise. Define the matrix $Z$ on words of length $r$ by

Z(u,u')=\sum_{h:[k]\to[d]}X((u,h),(u',h)),

and define $K_Z((u,(v,w)),(u',(v',w')))=Z(u,u')$ when $(v,w)=(v',w')$ , and zero otherwise. Then

C L_X C=K_Z C.

The assertion imposes no further condition on $X$ and permits $r=0$ , in which case the words $u,u'$ are empty.

Human review

Endorsed by Shuze Chen · Oct 29, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 29, 2026
Confirmed by the mission captain (proposal self-audit).

View graph