Optimal physical recovery duality

Open

QAlgorithms.Papers.Independent.Intakethird100.P44.optimal_physical_recovery

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 P$ and $\mathcal Q$ be canonical Hilbert–Schmidt projections onto the input and output physical dagger algebras. Suppose $\mathcal N$ is physical, $\mathcal Q\mathcal N\mathcal P=\mathcal Q\mathcal N$ , and let $\mathcal M$ be any channel from the input space to itself. Choose any complementary channels of the composite maps $\mathcal Q\mathcal N$ and $\mathcal P\mathcal M$ , including complements equivalent by CPTP postprocessing in both directions. Then the attained maxima satisfy

\max_{\mathcal P\mathcal R\mathcal Q=\mathcal P\mathcal R}F(\mathcal R\mathcal N,\mathcal P\mathcal M)=\max_{\mathcal S}F(\widehat{\mathcal Q\mathcal N},\mathcal S\widehat{\mathcal P\mathcal M}).

All optimizers are CPTP, and the dual optimizer is unconstrained. This characterizes physical recovery without assuming $\mathcal M=\mathcal P\mathcal M$ .

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.5, Corollary 5, Eq.(13). The hats cover QN and PM, respectively.
M is arbitrary; it is NOT required to satisfy M=PM. -/
theorem optimal_physical_recovery [Nonempty H] [Nonempty K]
    [Nonempty E] [Nonempty F]
    (P : ObservableAlgebra H) (Q : ObservableAlgebra K)
    (N : Superop H K) (M : Superop H H) (hN : IsChannel N) (hM : IsChannel M)
    (hphys : IsPhysicalChannel P.project Q.project N)
    (CN : Superop H E) (CM : Superop H F)
    (hCN : IsGeneralizedComplement (Q.project ∘ N) CN)
    (hCM : IsGeneralizedComplement (P.project ∘ M) CM) (c : Comparison H) :
    SameMaximum
      (fun R : Superop K H => IsChannel R ∧ IsPhysicalChannel Q.project P.project R)
      (fun R => comparisonRootFidelity c (R ∘ N) (P.project ∘ M))
      (fun S : Superop F E => IsChannel S)
      (fun S => comparisonRootFidelity c CN (S ∘ CM)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P44

end

Source

Approximate recovery with locality and symmetry constraints, arXiv:1806.10324v2, PDF p. 5, Corollary 5, Eq.(13): optimal physical recovery

Read-back

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

Let $H,K,E,F$ be nonempty finite index types with decidable equality, and write $\operatorname{Mat}(I)$ for the complex matrices indexed by $I\times I$ . Here a channel $\Phi:\operatorname{Mat}(I)\to\operatorname{Mat}(J)$ means a map admitting a finite representation $\Phi(X)=\sum_a V_aXV_a^\dagger$ with $\sum_a V_a^\dagger V_a=I$ . Let $P,Q$ consist respectively of complex star subalgebras $\mathcal A_P\subseteq\operatorname{Mat}(H)$ , $\mathcal A_Q\subseteq\operatorname{Mat}(K)$ and channel maps $\mathcal P,\mathcal Q$ whose outputs lie in those algebras and satisfy $\operatorname{tr}((X-\mathcal P(X))^\dagger Y)=0$ for every $X$ and $Y\in\mathcal A_P$ , and likewise for $\mathcal Q,\mathcal A_Q$ . Let $N:H\to K$ and $M:H\to H$ , understood as maps on matrices, be channels satisfying $\mathcal Q(N(\mathcal P(X)))=\mathcal Q(N(X))$ for every $X$ . Let $C_N:H\to E$ and $C_M:H\to F$ be generalized complements of $\mathcal Q\circ N$ and $\mathcal P\circ M$ , respectively: for each corresponding pair $(D,C)$ , there is a finite Kraus family $V_a$ representing $D$ , with $\sum_aV_a^\dagger V_a=I$ , and channels $T,S$ such that $C=T\circ\widehat D$ and $\widehat D=S\circ C$ , where $\widehat D(X)_{ab}=\operatorname{tr}(V_aXV_b^\dagger)$ . Choose a comparison $c$ , either a density matrix $\rho$ on $H$ , or a positive integer $k$ and a matrix $W:\mathbb C^k\to\mathbb C^H$ with $W^\dagger W=I$ . Define $F_{\mathrm r}(A,B)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt A\,B\sqrt A}$ , using continuous functional calculus, and let $\Omega_\rho$ have entries $(\Omega_\rho)_{(i,j),(u,v)}=(\sqrt\rho)_{ji}\overline{(\sqrt\rho)_{vu}}$ . For the fixed comparison put $F_c(D_1,D_2)=F_{\mathrm r}((\mathrm{id}\otimes D_1)(\Omega_\rho),(\mathrm{id}\otimes D_2)(\Omega_\rho))$ ; for the code comparison take the infimum of this expression over all density matrices on $\mathbb C^k$ , replacing $D_i$ by $D_i\circ(X\mapsto WXW^\dagger)$ . The identity extension applies $D_i$ to each matrix block indexed by the reference coordinates. Then there exist channels $R:K\to H$ and $S:F\to E$ , with $\mathcal P(R(\mathcal Q(X)))=\mathcal P(R(X))$ for every $X$ , such that

F_c(R\circ N,\mathcal P\circ M)=F_c(C_N,S\circ C_M),

and this common value is at least the first expression for every channel $R$ satisfying that same physical condition and at least the second expression for every channel $S:F\to E$ . Thus both maxima are attained.

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