Lemma 10 / Eq.(83): channels from a purification and fixed-marginal states

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.purification_channel_states

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

prove2quantum

All systems have finite positive dimension and fixed computational bases. Matrix order is Loewner order and logarithms are base two.

Let $|\psi\rangle_{AR}$ be a normalized pure state, and let $\rho_{AB}$ be a density matrix with $\psi_A=\rho_A$ . For every $\varepsilon\ge0$ ,

\{(\mathrm{id}_A\otimes\mathcal N)(|\psi\rangle\langle\psi|):\mathcal N:R\to B\text{ CPTP},\ P((\mathrm{id}\otimes\mathcal N)(\psi),\rho)\le\varepsilon\}=\{\sigma_{AB}\text{ density}:\sigma_A=\rho_A,\ P(\sigma,\rho)\le\varepsilon\}.

Here $P$ is purified distance. These are sets of states; purification dimension is arbitrary and no full-rank assumption is made.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P65

Formal statement

noncomputable section

open Filter QAlgorithms

open scoped BigOperators Matrix ComplexConjugate ComplexOrder Topology

namespace QAlgorithms.Papers.Independent.Intakethird100.P65

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Dependency50.P09 (transposeBob)

open QAlgorithms.Papers.Independent.Dependency50.P35 (maxRelative)

open QAlgorithms.Papers.Independent.Independent2.P01 (dampingKraus damping)

open QAlgorithms.Papers.Independent.Gap48.P33 (phaseFlipChannel)

open QAlgorithms.Papers.Independent.Information100.P06 (Below)

open QAlgorithms.Papers.Independent.Information100.P34 (choi)

open QAlgorithms.Papers.Independent.Information100.P62 (Stochastic)

open QAlgorithms.Papers.Independent.Information100.P63 (Mat)

open QAlgorithms.Papers.Independent.Information100.P67 (IsSubnormalized purifiedDistance)

open QAlgorithms.Papers.Independent.Information100.P69 (replacer permute)

open QAlgorithms.Papers.Independent.Information100.P71 (diamond channelPower channelRelative)

open QAlgorithms.Papers.Independent.Support50.P39 (quantumMutualInformation)

variable {A B C D R : Type} [Fintype A] [DecidableEq A]
  [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C]
  [Fintype D] [DecidableEq D] [Fintype R] [DecidableEq R]

variable [Nonempty A] [Nonempty B] [Nonempty C] [Nonempty D] [Nonempty R]

/-- Lemma 10, Eq.(83), PDF p.19: equality of sets of STATES, allowing a singular
marginal and arbitrary finite purification dimension R. -/
theorem purification_channel_states (psi : EuclideanSpace ℂ (A × R)) (hpsi : ‖psi‖ = 1)
    (rho : Mat (A × B)) (hrho : IsDensityMatrix rho)
    (hmarg : traceRight (pureDensity psi) = traceRight rho) (e : ℝ) (he : 0 ≤ e) :
    {sigma : Mat (A × B) | ∃ N : Superop R B, IsChannel N ∧
      sigma = idTensorSuperop N (pureDensity psi) ∧ purifiedDistance sigma rho ≤ e} =
    {sigma : Mat (A × B) | IsDensityMatrix sigma ∧
      purifiedDistance sigma rho ≤ e ∧ traceRight sigma = traceRight rho} := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P65

end

Source

Quantum Channel Simulation and the Channel's Smooth Max-Information, arXiv:1807.05354v2, PDF p. 19, Lemma 10 / Eq.(83): channels from a purification and fixed-marginal states

Read-back

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

For finite types $A,R,B$ with decidable equality, every vector $\psi\in\mathbb C^{A\times R}$ with $\|\psi\|=1$ , every positive semidefinite matrix $\rho$ on $A\times B$ with $\operatorname{tr}\rho=1$ , and every real $e\ge0$ , assume that $\operatorname{Tr}_R(\psi\psi^\dagger)=\operatorname{Tr}_B\rho$ . Then the following two sets of matrices on $A\times B$ are equal:

\left\{\sigma:\ \exists N:\operatorname{Mat}(R)\to\operatorname{Mat}(B) \text{ a channel},\ \sigma=(\mathrm{id}_A\otimes N)(\psi\psi^\dagger),\ P(\sigma,\rho)\le e\right\} = \left\{\sigma:\ \sigma\succeq0,\ \operatorname{tr}\sigma=1,\ P(\sigma,\rho)\le e,\ \operatorname{Tr}_B\sigma=\operatorname{Tr}_B\rho\right\}.

Here $(\psi\psi^\dagger)_{x,y}=\psi_x\overline{\psi_y}$ , a channel is a map $N(X)=\sum_{j=0}^{m-1}K_jXK_j^\dagger$ for some natural $m$ , with $K_j$ of size $B\times R$ and $\sum_jK_j^\dagger K_j=I_R$ , and $(\mathrm{id}_A\otimes N)(X)_{(a,b),(a',b')}=N(X_{(a,\cdot),(a',\cdot)})_{b,b'}$ . Partial traces sum over the discarded diagonal index. The distance used is

P(X,Y)=\sqrt{1-\left( \operatorname{Re}\operatorname{tr}\sqrt{\sqrt X\,Y\sqrt X} +\sqrt{(1-\operatorname{Re}\operatorname{tr}X)(1-\operatorname{Re}\operatorname{tr}Y)} \right)^2},

with square roots defined by continuous functional calculus. The assertion includes $e=0$ and imposes no upper bound on $e$ . The normalization hypotheses cannot hold when any of the relevant registers $A,R,B$ is empty.

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