Classical wiretap embedding, Kraus family and dilation recovery

Open

QAlgorithms.Papers.Independent.Intakethird100.P74.classical_embedding

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

prove2quantum

Let $X,Y,Z$ be finite classical alphabets with $X$ nonempty, and suppose $p(y,z\mid x)\ge0$ and $\sum_{y,z}p(y,z\mid x)=1$ for every $x$ . Embed the symbols as orthonormal quantum basis vectors. Define

\mathcal N_C(\rho)=\sum_{x,y,z}\langle x|\rho|x\rangle p(y,z\mid x) |y,z\rangle\langle y,z|, \qquad K_{xyz}=\sqrt{p(y,z\mid x)}|y,z\rangle\langle x|.

The family $\{K_{xyz}\}$ is normalized, $\sum_{xyz}K_{xyz}^\dagger K_{xyz}=I$ , and defines a CPTP map. The explicit map

V|\psi\rangle=\sum_{x,y,z}\sqrt{p(y,z\mid x)}\langle x|\psi\rangle |y,z\rangle^{BE}|x,y,z\rangle^{S_2}

is an isometry. For every normalized density matrix $\rho$ ,

\sum_{xyz}K_{xyz}\rho K_{xyz}^\dagger =\mathcal N_C(\rho) =\operatorname{Tr}_{S_2}(V\rho V^\dagger).

This embeds a general finite classical wiretap channel, discarding off-diagonal input entries while keeping the dilation record in a shield unavailable to Eve.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P74

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P74

open QAlgorithms

open scoped ComplexConjugate Matrix

noncomputable section

local instance (p : Prop) : Decidable p := Classical.propDecidable p

variable {B E S1 S2 : Type}

variable [Fintype B] [Fintype E] [Fintype S1] [Fintype S2]

variable [DecidableEq B] [DecidableEq E] [DecidableEq S1] [DecidableEq S2]

/-- PDF p.6, Appendix A: for arbitrary finite classical alphabets, the printed Kraus
operators are normalized, their channel is Eq.(14), the explicit dilation is isometric,
and tracing its shield recovers Eq.(14) on every normalized input state. -/
theorem classical_embedding {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z]
    [DecidableEq X] [DecidableEq Y] [DecidableEq Z] [Nonempty X]
    (p : X → Y → Z → ℝ) (hp : ∀ x y z, 0 ≤ p x y z)
    (hnorm : ∀ x, ∑ y, ∑ z, p x y z = 1) :
    IsKrausFamily (classicalKraus p) ∧
    IsChannel (classicalEmbedding p) ∧
    (classicalDilation p)ᴴ * classicalDilation p = 1 ∧
    (∀ rho : Matrix X X ℂ, IsDensityMatrix rho →
      krausApply (classicalKraus p) rho = classicalEmbedding p rho ∧
      traceRight (classicalDilation p * rho * (classicalDilation p)ᴴ) =
        classicalEmbedding p rho) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P74

Source

Polar codes for private classical communication, arXiv:1203.5794v1, PDF p. 6, Appendix A, unnumbered: classical wiretap embedding and explicit dilation

Read-back

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

For finite types $X,Y,Z$ with decidable equality, with $X$ nonempty, let $p:X\times Y\times Z\to\mathbb R$ satisfy $p(x,y,z)\ge0$ for every $x,y,z$ and $\sum_y\sum_zp(x,y,z)=1$ for every $x$ . Define matrices $K_{x,y,z}:\mathbb C^X\to\mathbb C^{Y\times Z}$ and $V:\mathbb C^X\to\mathbb C^{(Y\times Z)\times(X\times Y\times Z)}$ by

(K_{x,y,z})_{(y',z'),a}= \begin{cases}\sqrt{p(x,y,z)},&(y',z')=(y,z),\ a=x,\\0,&\text{otherwise},\end{cases}

V_{((y',z'),(x,y,z)),a}= \begin{cases}\sqrt{p(x,y,z)},&(y',z')=(y,z),\ a=x,\\0,&\text{otherwise},\end{cases}

and define $\Phi$ on every complex $X\times X$ matrix by

[\Phi(\rho)]_{(y,z),(y',z')}= \begin{cases} \displaystyle\sum_x\rho_{x,x}p(x,y,z),&(y,z)=(y',z'),\\ 0,&\text{otherwise}. \end{cases}

Then all of the following hold:

\sum_{x,y,z}K_{x,y,z}^*K_{x,y,z}=I_X,\qquad V^*V=I_X;

$\Phi$ is a channel, meaning that there exist a natural number $r$ and matrices $L_j:\mathbb C^X\to\mathbb C^{Y\times Z}$ with $\sum_{j<r}L_j^*L_j=I_X$ and $\Phi(\rho)=\sum_{j<r}L_j\rho L_j^*$ for every complex matrix $\rho$ ; and, for every positive semidefinite complex $X\times X$ matrix $\rho$ with $\operatorname{tr}\rho=1$ ,

\sum_{x,y,z}K_{x,y,z}\rho K_{x,y,z}^*=\Phi(\rho), \qquad \operatorname{Tr}_{X\times Y\times Z}(V\rho V^*)=\Phi(\rho).

The partial trace in the last equality sums over the second row-and-column factor $X\times Y\times Z$ . Nonemptiness of $Y$ and $Z$ is not separately assumed, but if either is empty the normalization hypotheses cannot hold because $X$ is nonempty.

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