IV B: soundness of a candidate degrading-map extension certificate

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.extensionCertificate

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

prove2quantum

Let $P\succeq0$ be an operator on finite nonempty systems $A\otimes B$ , in a fixed product basis. Make exact copies $E_1=A$ , $E_2=B$ , and construct $|\psi\rangle=\operatorname{vec}\sqrt P$ , with the physical $AB$ registers first. Let $N:E_1\to B'$ be any specified completely positive trace-preserving channel, where $B'$ is a copy of $B$ , and put $E=N\circ\operatorname{Tr}_{E_2}$ . Let $W=\operatorname{Tr}_B|\psi\rangle\langle\psi|$ . If the tested antidegrading equality holds,

(\mathrm{id}_A\otimes E)(W)=P,

then $\operatorname{Tr}_{E_1E_2}|\psi\rangle\langle\psi|=P$ , and the constructed operator

R=(\mathrm{id}_{AB}\otimes E)(|\psi\rangle\langle\psi|)

is positive and has both $AB$ and $AB'$ marginals equal to $P$ . Hence $P$ is Bob-extendable. The complementary map is not assumed trace preserving. This is a soundness certificate for a candidate $N$ , including $P=0$ , and does not specify the particular experimental map or assert nonextendability when a candidate fails.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P30

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P30

open scoped BigOperators Matrix ComplexConjugate ComplexOrder

attribute [local instance] Classical.propDecidable Classical.decEq

variable {I J K L A B : Type}

variable [Fintype I] [Fintype J] [Fintype K] [Fintype L]

variable [Fintype A] [Fintype B]

/-- PDF pp.8–9, IV B steps 1–3: soundness for any candidate channel N satisfying
the tested antidegrading equality. This does not identify the experimental special N. -/
theorem extensionCertificate [Nonempty A] [Nonempty B]
    (P : Matrix (A × B) (A × B) ℂ) (hP : P.PosSemidef)
    (N : Superop A B) (hN : IsChannel N)
    (htest : idTensorSuperop (candidateDegrader N) (complementaryOperator P) = P) :
    traceRight (pureDensity (vectorPurification P)) = P ∧
    IsBobCopyExtension P (candidateExtension P N) ∧ BobExtendible P := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P30

end

Source

Numerical evidence for bound secrecy from two-way post-processing in quantum key distribution, arXiv:1612.07734v2, PDF p. 9, IV B: soundness of a candidate degrading-map extension certificate

Read-back

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

For finite, nonempty index types $A,B$ with decidable equality, let $P$ be a positive semidefinite complex matrix indexed by $A\times B$ . Let $N$ be a function from complex matrices indexed by $A$ to complex matrices indexed by $B$ that is a channel in the following explicit sense: there exist a natural number $r$ and matrices $F_j$ , with rows indexed by $B$ and columns indexed by $A$ , such that

\sum_{j=0}^{r-1}F_j^{*}F_j=I_A, \qquad N(X)=\sum_{j=0}^{r-1}F_jXF_j^{*} \quad\text{for every matrix }X.

Put $S=\sqrt P$ , obtained by the real continuous functional calculus, and define

v(x,y)=S_{x,y},\qquad K_{(a,x),(a',y)}=\sum_{c\in B}S_{(a,c),x}\overline{S_{(a',c),y}},

for $x,y\in A\times B$ . Assume that, for every $a,a'\in A$ and $b,b'\in B$ ,

\bigl[N(H^{a,a'})\bigr]_{b,b'}=P_{(a,b),(a',b')}, \qquad H^{a,a'}_{u,u'}=\sum_{c\in B}K_{(a,(u,c)),(a',(u',c))}.

Define $E$ , indexed by $(A\times B)\times B$ , by

E_{(x,b),(y,b')}=\bigl[N(Y^{x,y})\bigr]_{b,b'}, \qquad Y^{x,y}_{u,u'}=\sum_{c\in B}S_{x,(u,c)}\overline{S_{y,(u',c)}}.

Then the partial trace of $vv^{*}$ over its second $A\times B$ factor equals $P$ , explicitly

\sum_{y\in A\times B}v(x,y)\overline{v(x',y)}=P_{x,x'}.

Furthermore, $E$ is positive semidefinite and satisfies both marginal identities

\sum_cE_{((a,b),c),((a',b'),c)} = \sum_cE_{((a,c),b),((a',c),b')} =P_{(a,b),(a',b')}.

Consequently, such a positive semidefinite Bob-copy extension of $P$ exists. There is no trace-one hypothesis on $P$ ; in particular, $P=0$ is included.

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