Tensor-product local recovery duality

Open

QAlgorithms.Papers.Independent.Intakethird100.P44.tensor_local_duality

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

prove2quantum

All Hilbert spaces are finite dimensional and nonzero, and every channel is completely positive and trace preserving on the full matrix algebra. Here $F$ denotes either root entanglement fidelity $F_\rho$ for any normalized input density $\rho$ , with an identity reference retained, or worst-case root entanglement fidelity $F_W$ over all normalized logical densities for an arbitrary isometry $W$ . Let $\mathcal N_A$ be a channel on $H_A$ and let $\widehat{\mathcal N_A}$ be any complementary channel to an environment $E$ . The comparison domain is the joint system $H_A\otimes H_B$ ; a code may be entangled across the factors. Put $\mathcal D_\sigma(X)=\sigma\operatorname{Tr}X$ . Both maxima are attained and

\max_{\mathcal R_A}F((\mathcal R_A\mathcal N_A)\otimes\mathrm{id}_B,\mathrm{id}_{AB})=\max_{\sigma\succeq0,\,\operatorname{Tr}\sigma=1}F(\widehat{\mathcal N_A}\otimes\mathrm{id}_B,\mathcal D_\sigma\otimes\mathrm{id}_B).

The recovery acts only on $A$ . This independently stated tensor specialization retains arbitrary joint encodings.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P44

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P44

open scoped Matrix ComplexConjugate ComplexOrder

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

open QAlgorithms.Papers.Independent.Information100.P67 (mapFirst)

open QAlgorithms.Papers.Independent.Claimed50.P48 (operatorTraceDual)

open QAlgorithms.Papers.Independent.Renew46.P43 (purification)

variable {H K L J E F B : Type*}

variable [Fintype H] [DecidableEq H] [Fintype K] [DecidableEq K]

variable [Fintype L] [DecidableEq L] [Fintype J] [DecidableEq J]

variable [Fintype E] [DecidableEq E] [Fintype F] [DecidableEq F]

variable [Fintype B] [DecidableEq B]

/-- PDF p.9, Eq.(48), for either fidelity, including joint entangled codes. -/
theorem tensor_local_duality [Nonempty H] [Nonempty B] [Nonempty E]
    (N : Superop H H) (hN : IsChannel N) (CN : Superop H E)
    (hCN : IsGeneralizedComplement N CN) (c : Comparison (H × B)) :
    SameMaximum (fun R : Superop H H => IsChannel R)
      (fun R => comparisonRootFidelity c (mapFirst (R ∘ N)) (id : Superop (H × B) (H × B)))
      (fun sigma : Mat E => IsDensityMatrix sigma)
      (fun sigma => comparisonRootFidelity c (mapFirst CN)
        (mapFirst (constantChannel (H := H) sigma))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P44

end

Source

Approximate recovery with locality and symmetry constraints, arXiv:1806.10324v2, PDF p. 9, §IV D, Eq.(48): tensor-product local recovery duality

Read-back

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

Let $H,B,E$ be finite nonempty index types with decidable equality, let $N$ be a channel on $H$ , and let $C_N$ be a map from matrices on $H$ to matrices on $E$ satisfying the following generalized complement condition: there exist $m\geq0$ , matrices $A_j:\mathbb C^H\to\mathbb C^H$ with $\sum_jA_j^\dagger A_j=I$ and $N(X)=\sum_jA_jXA_j^\dagger$ , and channels $S:\mathbb C^{m\times m}\to\mathbb C^{E\times E}$ , $T:\mathbb C^{E\times E}\to\mathbb C^{m\times m}$ , such that $C_N=S\circ C_A$ and $C_A=T\circ C_N$ , where $C_A(X)_{ij}=\operatorname{tr}(A_iXA_j^\dagger)$ . Choose a comparison $c$ on $H\otimes B$ : either a specified density matrix $\rho$ , or a positive integer $k$ and an isometry $W:\mathbb C^k\to\mathbb C^H\otimes\mathbb C^B$ . For maps $F,G$ with the same input and output spaces, define

\mathcal F_\rho(F,G)= \operatorname{Re}\operatorname{tr} \sqrt{\sqrt{(\mathrm{id}\otimes F)(\Pi_\rho)} \,(\mathrm{id}\otimes G)(\Pi_\rho)\, \sqrt{(\mathrm{id}\otimes F)(\Pi_\rho)}}, \qquad \Pi_\rho=|v_\rho\rangle\langle v_\rho|, \quad v_\rho(i,j)=(\sqrt\rho)_{ji}.

For the fixed comparison set $\mathcal F_c=\mathcal F_\rho$ ; for the code comparison set $\mathcal F_c(F,G)=\inf_\rho\mathcal F_\rho(F\circ\operatorname{Ad}_W,G\circ\operatorname{Ad}_W)$ , with the infimum over all $k\times k$ density matrices and $\operatorname{Ad}_W(X)=WXW^\dagger$ . Then there exist a channel $R_*$ on $H$ and a density matrix $\sigma_*$ on $E$ such that

\mathcal F_c((R_*\circ N)\otimes\mathrm{id}_B,\mathrm{id}_{H\otimes B}) = \mathcal F_c(C_N\otimes\mathrm{id}_B,K_{\sigma_*}\otimes\mathrm{id}_B),

and this common value is at least the left expression for every channel $R$ , and at least the right expression for every density matrix $\sigma$ , where $K_\sigma(X)=\operatorname{tr}(X)\sigma$ . Density matrices are positive semidefinite matrices of trace $1$ ; channels are maps with finite Kraus representations whose matrices satisfy $\sum_jE_j^\dagger E_j=I$ . Tensoring a map with an identity means applying it to each matrix block indexed by the unchanged factor. Thus both maxima are attained, whereas attainment of the infimum within a code comparison is not asserted.

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