Theorem 4.21 — extremality criterion for unital channels

Open

WatrousTQI.unital_extreme_kraus_criterion

by Mrnaiq · Nov 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

convexitymixed-unitaryquantum-channelsquantum-information

Let $d,m>0$ , let $\Phi$ be a trace-preserving completely positive map with $\Phi(I_d)=I_d$ , and let $A_0,\ldots,A_{m-1}$ be a complex-linearly independent Kraus family representing $\Phi$ on every operator. Then $\Phi$ is an extreme point of the real convex set of all unital channels if and only if the $m^2$ pairs $(A_b^\dagger A_a,A_aA_b^\dagger)$ are complex-linearly independent. Pairs of matrices encode the block-diagonal operators in equation (4.147) through the natural complex-linear isomorphism; both blocks and the order of their factors are retained.

Preamble

import Mathlib
import Definitions.Def_QAlgorithms_Defs_Channel
import Definitions.Def_WatrousTQI_UnitalChannels
set_option autoImplicit false
noncomputable section
open scoped Matrix ComplexConjugate BigOperators

Formal statement

namespace WatrousTQI

theorem unital_extreme_kraus_criterion (d m : ℕ) (hd : 0 < d) (hm : 0 < m)
    (Φ : QAlgorithms.Superop (Fin d) (Fin d))
    (hΦ : QAlgorithms.IsChannel Φ)
    (hu : Φ (1 : Matrix (Fin d) (Fin d) ℂ) = 1)
    (A : Fin m → Matrix (Fin d) (Fin d) ℂ)
    (hLI : LinearIndependent ℂ A)
    (hrep : ∀ X, Φ X = QAlgorithms.krausApply A X) :
    Φ ∈ (unitalChannels d).extremePoints ℝ ↔
      LinearIndependent ℂ (fun ab : Fin m × Fin m =>
        ((A ab.2)ᴴ * A ab.1, A ab.1 * (A ab.2)ᴴ)) := by sorry

end WatrousTQI

Source

John Watrous, The Theory of Quantum Information, Cambridge University Press, 2018, Chapter 4. https://cs.uwaterloo.ca/~watrous/TQI/TQI.pdf; Theorem 4.21, equations (4.146)–(4.147), printed p.225 (PDF p.233).

Read-back

What the Lean code literally says, in plain math · GPT-6 (Codex)

For every pair of natural numbers $d,m$ with $0<d$ and $0<m$ , every function $\Phi:M_d(\mathbb C)\to M_d(\mathbb C)$ , and every indexed family $A=(A_j)_{j\in\{0,\ldots,m-1\}}$ of complex $d\times d$ matrices, assume that $\Phi$ is a channel in the following precise sense: there exist a natural number $n$ and matrices $B_0,\ldots,B_{n-1}$ such that $\sum_r B_r^*B_r=I_d$ and $\Phi(X)=\sum_r B_rXB_r^*$ for every complex $d\times d$ matrix $X$ ; assume also that $\Phi(I_d)=I_d$ , that $A$ is complex linearly independent (if $\sum_j c_jA_j=0$ for complex coefficients $c_j$ , then every $c_j=0$ ), and that $\Phi(X)=\sum_j A_jXA_j^*$ for every $X$ . Then $\Phi$ is an extreme point over the real scalars of the set of all channels $\Psi:M_d(\mathbb C)\to M_d(\mathbb C)$ satisfying $\Psi(I_d)=I_d$ , where “channel” has exactly the finite matrix representation and normalization just specified, if and only if the family of ordered pairs of matrices $(A_b^*A_a,\,A_aA_b^*)$ , indexed by every ordered pair $(a,b)\in\{0,\ldots,m-1\}^2$ , is complex linearly independent in $M_d(\mathbb C)\times M_d(\mathbb C)$ . Here $^*$ denotes conjugate transpose; extremality means that $\Phi$ belongs to that set and, for any two members $\Psi,\Omega$ of the set and any real $t$ with $0<t<1$ , the pointwise equality $\Phi=t\Psi+(1-t)\Omega$ implies $\Psi=\Phi=\Omega$ ; and the linear independence on the right means that, for any complex coefficients $c_{ab}$ , the simultaneous equalities $\sum_{a,b}c_{ab}A_b^*A_a=0$ and $\sum_{a,b}c_{ab}A_aA_b^*=0$ imply $c_{ab}=0$ for every ordered pair. Both diagonal pairs $a=b$ and both orders of distinct indices are included. The assumptions exclude $d=0$ and $m=0$ ; the definition of channel itself permits a representation indexed by $n=0$ , with empty sums equal to zero, but such a representation cannot satisfy $\sum_r B_r^*B_r=I_d$ when $d>0$ . The conclusion is conditional on all the stated hypotheses, including the independence of $A$ ; it asserts nothing for families that fail them.

Human review

Endorsed by Shuze Chen · Nov 12, 2026
Confirmed by the moderator at approval.
Endorsed by Mrnaiq · Nov 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph