Theorem 2.31 proof — Hermitian witness for Kraus-product dependence

Open

WatrousTQI.kraus_dependence_hermitian_witness

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

convexitykraus-operatorsprove2quantumquantum-channels

For positive input and output dimensions and a nonempty finite family $A_0,\ldots,A_{m-1}$ of rectangular complex matrices, complex linear dependence of the indexed family $(A_b^\dagger A_a)_{a,b}$ yields a nonzero Hermitian coefficient matrix:

\exists H=H^\dagger\ne0:\quad\sum_{a,b}H_{ab}A_b^\dagger A_a=0.

This algebraic step does not require channel normalization or independence of the original Kraus operators. It is extracted from equations (2.184)–(2.187), whose argument uses neither condition.

Preamble

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

Formal statement

namespace WatrousTQI
theorem kraus_dependence_hermitian_witness {dx dy m : ℕ}
    (hdx : 0 < dx) (hdy : 0 < dy) (hm : 0 < m)
    (A : Fin m → Matrix (Fin dy) (Fin dx) ℂ)
    (hdep : ¬ LinearIndependent ℂ (fun ab : Fin m × Fin m => (A ab.2)ᴴ * A ab.1)) :
    ∃ H : Matrix (Fin m) (Fin m) ℂ,
      H.IsHermitian ∧ H ≠ 0 ∧ ∑ a, ∑ b, H a b • ((A b)ᴴ * A a) = 0 := 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; Proof of Theorem 2.31, equations (2.184)–(2.187), printed p.98.

Read-back

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

For all positive natural numbers $d_x,d_y,m$ and every family $(A_a)_{a\in\{0,\ldots,m-1\}}$ of complex $d_y\times d_x$ matrices, if the family of $m^2$ complex $d_x\times d_x$ matrices $(A_b^*A_a)_{(a,b)\in\{0,\ldots,m-1\}^2}$ is not linearly independent over $\mathbb C$ , then there exists a complex $m\times m$ matrix $H$ such that $H=H^*$ , $H\ne0$ , and $\sum_{a=0}^{m-1}\sum_{b=0}^{m-1}H_{ab}(A_b^*A_a)=0$ . Here a star denotes conjugate transpose, multiplication by $H_{ab}$ is complex scalar multiplication, and the final zero is the zero $d_x\times d_x$ matrix. The dependence hypothesis means there is a nonzero complex coefficient array giving a zero linear combination of those ordered-pair-indexed products. The conclusion requires a nonzero Hermitian coefficient array with the same vanishing sum; it imposes no positivity, normalization, or rank condition on $H$ or on the $A_a$ . All three dimensions are positive, including the permitted value $m=1$ when its dependence hypothesis holds, and the family may include zero matrices.

View graph