Simulation of local CPTP protocols by local unitaries

Open

QAlgorithms.Papers.Independent.Intakethird100.P81.local_cptp_simulation

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $P$ be a finite two-party protocol on separate finite classical input sets. Its $k$ alternating messages have fixed senders and fixed transmitted wires; each local operation is a complex-linear CPTP map controlled only by its owner's input. Its normalized initial work state is independent of both inputs, and its final output measurement belongs to the announcing player. Let $c(P)$ be the number of transmitted qubits.

There is a protocol $Q$ using local unitaries and additional private blank qubits, with the same starting player, number of messages and announcing player, such that

c(Q)\le c(P),\qquad \Pr_Q[o\mid x,y]=\Pr_P[o\mid x,y]\quad\text{for every }x,y,o.

The initial state of $Q$ is exactly the original state embedded on ownership-preserving wires, tensor additional zero qubits. Thus the simulation introduces no stronger prior entanglement or input-dependent advice. This expresses equality of full output distributions, not merely preservation of one success probability.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P81

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ENNReal

attribute [local instance] Classical.propDecidable

namespace QAlgorithms.Papers.Independent.Intakethird100.P81

open QAlgorithms.Papers.Independent.Information100.P54 (relativeEntropyBits)

open QAlgorithms.Papers.Independent.Bridge50.P44 (ClassicalFirst)

/-- Unnumbered simulation claim, PDF p.6: arbitrary local CPTP operations can be purified
using only additional private blank qubits, preserving every output probability, rounds and cost. -/
theorem local_cptp_simulation {X Y O : Type} [Fintype X] [Fintype Y] [Fintype O]
    (P : ChannelProtocol X Y O) (start : Party) (k : ℕ) (hP : P.valid start k) :
    ∃ Q : QuantumProtocol X Y O, Q.valid start k ∧ BlankExtension P Q ∧
      Q.cost ≤ P.cost ∧ Q.outputParty = P.outputParty ∧
      ∀ x y o, Q.probability x y o = P.probability x y o := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P81

end

Source

On rounds in quantum communication, arXiv:quant-ph/0004100v5, PDF p. 6, Unnumbered model simulation paragraph

Read-back

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

For arbitrary finite types $X,Y,O$ , each equipped with a finite enumeration, a channel protocol $P$ , a starting party $s$ , and a natural number $k$ , suppose $P$ is valid: its initial vector has norm one; it has exactly $k$ rounds alternating speakers from $s$ ; every sent wire is currently owned by its speaker; for every input pair each selected round operation has a finite Kraus representation $\rho\mapsto\sum_jE_j\rho E_j^\dagger$ , with $\sum_jE_j^\dagger E_j=I$ and each $E_j$ acting within the current speaker's wires; and its selected final measurement consists of positive semidefinite matrices summing to the identity, each acting within its output party's final wires. Here selection uses the speaker's or output party's own input, and ownership changes by assigning sent wires to the other party. Then there exists a quantum protocol $Q$ on the same input and outcome types with a norm-one initial vector and exactly $k$ alternating rounds from $s$ , whose selected round matrices are unitary and act within the current speaker's wires, whose sent wires are owned by that speaker, and whose final measurement is positive semidefinite, sums to the identity, and acts within its output party's final wires; moreover, there is an owner-preserving injection $e$ of $P$ 's initial wires into $Q$ 's such that $Q$ 's initial amplitude at $z$ is $P$ 's initial amplitude at $z\circ e$ when all wires outside the image are false, and zero otherwise; the sum of sent-set sizes in $Q$ is at most that in $P$ ; their output parties agree; and for every $x\in X,y\in Y,o\in O$ ,

\operatorname{Re}\operatorname{tr}\!\left(M^Q_o(x,y)\, \psi^Q_{x,y}(\psi^Q_{x,y})^\dagger\right) = \operatorname{Re}\operatorname{tr}\!\left(M^P_o(x,y)\rho^P_{x,y}\right).

Here $\psi^Q_{x,y}$ is obtained by applying $Q$ 's selected round unitaries in list order to its initial vector, while $\rho^P_{x,y}$ is obtained by applying $P$ 's selected round maps in list order to the matrix with entries $P.\mathrm{initial}(u)\overline{P.\mathrm{initial}(v)}$ . In all the locality conditions, acting within $S$ means being the extension of a matrix on injectively selected wires contained in $S$ , with entries zero between strings differing outside those wires and the selected matrix's entries otherwise. The assertion includes $k=0$ , zero original wires, and rounds sending no wires; it bounds neither $Q$ 's wire count nor its local computational work. Empty input types are included, in which case the equality quantified over input pairs, and the corresponding input-indexed validity conditions, are vacuous.

Human review

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

View graph