Theorem 2.31 — Choi’s characterization of extreme quantum channels

Open

WatrousTQI.channel_extreme_kraus_criterion

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

convexitykraus-operatorsprove2quantumquantum-channels

Let $\Phi:M_{d_X}(\mathbb C)\to M_{d_Y}(\mathbb C)$ be a quantum channel on arbitrary positive finite dimensions. Suppose $A_0,\ldots,A_{m-1}$ form a complex-linearly independent Kraus representation of $\Phi$ on every input matrix. Then

\Phi\in\operatorname{ext}_{\mathbb R}\mathcal C(d_X,d_Y)\quad\Longleftrightarrow\quad(A_b^\dagger A_a)_{a,b}\text{ is linearly independent over }\mathbb C.

The convex set is the entire set of trace-preserving completely positive maps between these spaces. It is not restricted to unital, square, classical-to-quantum, or rank-one Kraus maps. Channels reuse the published finite-normalized-Kraus predicate.

Preamble

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

Formal statement

namespace WatrousTQI
theorem channel_extreme_kraus_criterion {dx dy m : ℕ}
    (hdx : 0 < dx) (hdy : 0 < dy) (hm : 0 < m)
    (Φ : QAlgorithms.Superop (Fin dx) (Fin dy))
    (hΦ : QAlgorithms.IsChannel Φ)
    (A : Fin m → Matrix (Fin dy) (Fin dx) ℂ)
    (hLI : LinearIndependent ℂ A)
    (hrep : ∀ X, Φ X = QAlgorithms.krausApply A X) :
    Φ ∈ ({Ψ : QAlgorithms.Superop (Fin dx) (Fin dy) | QAlgorithms.IsChannel Ψ}).extremePoints ℝ ↔
      LinearIndependent ℂ (fun ab : Fin m × Fin m => (A ab.2)ᴴ * A ab.1) := by sorry
end WatrousTQI

Source

John Watrous, The Theory of Quantum Information, Cambridge University Press, 2018, Section 2.2.4, printed pp.96–99. https://cs.uwaterloo.ca/~watrous/TQI/TQI.pdf; Theorem 2.31, equations (2.174)–(2.175), printed pp.97–99.

Read-back

What the Lean code literally says, in plain math · GPT-6 (exact model identifier unavailable)

For any types $\iota$ and $\kappa$ , a superoperator from $\iota$ to $\kappa$ is defined to be an arbitrary function from complex matrices with rows and columns indexed by $\iota$ to complex matrices with rows and columns indexed by $\kappa$ . This abbreviation imposes no finiteness assumptions, linearity, positivity, or normalization condition on the function.

For any types $K,\iota,\kappa$ , with specified finite enumerations of $K$ and $\kappa$ and decidable equality on $\iota$ , a family $(E_j)_{j\in K}$ of complex matrices with row index $\kappa$ and column index $\iota$ is defined to be a Kraus family precisely when $\sum_{j\in K}E_j^*E_j=I_{\iota}$ , where a star denotes conjugate transpose and $I_{\iota}$ is the identity matrix indexed by $\iota$ . No finiteness assumption on $\iota$ is made in this definition. Empty index types are permitted: for empty $K$ or empty $\kappa$ , the left side is zero, so the condition requires $0=I_{\iota}$ and holds exactly when $\iota$ is empty.

For any types $K,\iota,\kappa$ , with specified finite enumerations of $K$ and $\iota$ , and any family $(E_j)_{j\in K}$ of complex matrices with row index $\kappa$ and column index $\iota$ , its associated function on matrices is defined by $\rho\mapsto\sum_{j\in K}E_j\rho E_j^*$ . Its input is any complex matrix indexed by $\iota\times\iota$ , and its output is a complex matrix indexed by $\kappa\times\kappa$ . No finiteness assumption on $\kappa$ or Kraus-family normalization assumption is required for this definition. Empty $K$ gives the zero-valued function, and empty $\iota$ also makes every output zero.

For any types $\iota,\kappa$ , each with a specified finite enumeration and with decidable equality on $\iota$ , a function $\Phi$ from complex $\iota\times\iota$ matrices to complex $\kappa\times\kappa$ matrices is defined to be a channel precisely when there exist a natural number $r$ and matrices $(E_j)_{j\in\{0,\ldots,r-1\}}$ indexed by $\kappa\times\iota$ such that $\sum_{j=0}^{r-1}E_j^*E_j=I_{\iota}$ and, for every complex $\iota\times\iota$ matrix $\rho$ , $\Phi(\rho)=\sum_{j=0}^{r-1}E_j\rho E_j^*$ . This equality is required on all matrices, with no restriction to positive or normalized inputs. The existentially quantified $r$ may be zero; that case requires $0=I_{\iota}$ and the zero-valued function, and is therefore possible only when $\iota$ is empty. Empty input and output types are allowed by the definition; for empty input the channel condition gives the zero-valued function, while empty output with nonempty input cannot satisfy the normalization.

For every triple of positive natural numbers $d_x,d_y,m$ , every function $\Phi$ from complex $d_x\times d_x$ matrices to complex $d_y\times d_y$ matrices that is a channel, and every complex-linearly independent family $(A_a)_{a=0}^{m-1}$ of complex $d_y\times d_x$ matrices satisfying $\Phi(X)=\sum_{a=0}^{m-1}A_aXA_a^*$ for every complex $d_x\times d_x$ matrix $X$ , the following equivalence holds: $\Phi$ is an extreme point over $\mathbb R$ of the set of all such channels if and only if the family $(A_b^*A_a)_{(a,b)\in\{0,\ldots,m-1\}^2}$ is linearly independent over $\mathbb C$ . Here being a channel means that some finite family $(B_j)_{j=0}^{r-1}$ , for some natural number $r$ , satisfies $\sum_j B_j^*B_j=I_{d_x}$ and $\Phi(X)=\sum_j B_jXB_j^*$ for every complex input matrix $X$ ; the given family $A$ is assumed to represent $\Phi$ on all matrices and to be complex-linearly independent. Being an extreme point means that $\Phi$ belongs to this channel set and that for any two channels $\Psi_0,\Psi_1$ of these same dimensions and any real $t$ with $0<t<1$ , the equality $\Phi=t\Psi_0+(1-t)\Psi_1$ , interpreted pointwise on matrices, forces $\Psi_0=\Phi$ and $\Psi_1=\Phi$ . Both independence assertions concern finite linear combinations with arbitrary complex coefficients. The dimensions and the size $m$ of the specified representing family cannot be zero; $m=1$ is included, and no linear dependence of the specified family is allowed by the hypotheses. The representation size $r$ in the definition of a channel is not stipulated to equal $m$ ; although that definition permits $r=0$ , its normalization excludes $r=0$ here because $d_x>0$ .

View graph