Section 3.4: Lindblad dilation, Kraus isometry, and entropy preservation

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.lindbladDilation

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

prove2quantum

Every finite CPTP endomorphism $\Phi$ on $A$ admits a finite auxiliary system $B$ , a unit vector $\beta_B$ and a unitary $U_{AB}$ such that for every operator $X$ ,

\Phi(X)=\operatorname{Tr}_B\bigl[U_{AB}(X\otimes|\beta\rangle\langle\beta|)U_{AB}^{\dagger}\bigr].

For any finite normalized rectangular Kraus family $F_k:A\to A'$ , define $V_{(a',k),a}=(F_k)_{a',a}$ . Then

V^{\dagger}V=I,\quad\operatorname{Tr}_B(VXV^{\dagger})=\sum_kF_kXF_k^{\dagger},\quad S(V\rho V^{\dagger})=S(\rho).

For every density matrix $\rho$ , $V\rho V^{\dagger}$ and $\rho$ have the same nonzero eigenvalues with multiplicity. Only the endomorphism clause asserts a unitary on a single space.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P51

Formal statement

noncomputable section

open scoped Matrix ComplexOrder ComplexConjugate Matrix.Norms.L2Operator

open MeasureTheory

namespace QAlgorithms.Papers.Independent.Intakethird100.P51

attribute [local instance] Classical.propDecidable Classical.decEq

-- Exact interfaces from the frozen accepted library; no local redeclarations.

open QAlgorithms.Papers.Independent.Information100.P63 (Mat)

open QAlgorithms.Papers.Independent.Information100.P56 (entropy holevo IsLaw)

open QAlgorithms.Papers.Independent.Information100.P27 (average)

open QAlgorithms.Papers.Independent.Dependency50.P21 (relativeEntropy marginalAB channelAdjoint)

open QAlgorithms.Papers.Independent.Dependency50.P35 (marginalAC)

open QAlgorithms.Papers.Independent.Gap48.P19 (shannonNats)

open QAlgorithms.Papers.Independent.Gap48.P33 (measurementInformation)

section Statements

variable {A B C D J K O : Type}

variable [Fintype A] [Fintype B] [Fintype C] [Fintype D] [Fintype J] [Fintype K] [Fintype O]

variable [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]

variable [DecidableEq J] [DecidableEq K] [DecidableEq O]

/-- Section 3.4, equations (24)–(26), PDF pp.10–11: unitary endomorphism dilation
and rectangular Kraus isometry, with entropy and nonzero-spectrum preservation. -/
theorem lindbladDilation [Nonempty A] [Nonempty B] [Nonempty K] :
    (∀ Phi : Superop A A, IsChannel Phi →
      ∃ m : ℕ, 0 < m ∧ ∃ beta : EuclideanSpace ℂ (Fin m), ‖beta‖ = 1 ∧
        ∃ U : Mat (A × Fin m), Uᴴ * U = 1 ∧ U * Uᴴ = 1 ∧
          ∀ X : Mat A, Phi X = traceRight (U * Matrix.kronecker X (pureDensity beta) * Uᴴ)) ∧
    (∀ F : K → Matrix B A ℂ, IsKrausFamily F →
      (krausV F)ᴴ * krausV F = 1 ∧
      (∀ X : Mat A, traceRight (krausV F * X * (krausV F)ᴴ) = krausApply F X) ∧
      (∀ rho : Mat A, IsDensityMatrix rho →
        entropy (krausV F * rho * (krausV F)ᴴ) = entropy rho ∧
        ∀ z : ℂ, z ≠ 0 →
          Module.finrank ℂ (Module.End.eigenspace (krausV F * rho * (krausV F)ᴴ).mulVecLin z) =
          Module.finrank ℂ (Module.End.eigenspace rho.mulVecLin z))) := by sorry

end Statements

end QAlgorithms.Papers.Independent.Intakethird100.P51

end

Source

Inequalities for Quantum Entropy: A Review with Conditions for Equality, arXiv:quant-ph/0205064v2, PDF p. 10, Section 3.4: Lindblad dilation, Kraus isometry, and entropy preservation

Read-back

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

For finite nonempty index types $A,B,K$ , each with decidable equality, the following two assertions hold. First, every channel $\Phi$ from complex matrices on $A$ to matrices on $A$ —meaning a map admitting a finite representation $\Phi(X)=\sum_j E_jXE_j^\dagger$ with $\sum_jE_j^\dagger E_j=I_A$ —has a natural number $m>0$ , a Euclidean unit vector $\beta\in\mathbb C^m$ , and a matrix $U$ on $A\times\{0,\ldots,m-1\}$ satisfying $U^\dagger U=UU^\dagger=I$ , such that, for every complex matrix $X$ on $A$ ,

\Phi(X)=\operatorname{Tr}_{\{0,\ldots,m-1\}}\!\left(U(X\otimes|\beta\rangle\langle\beta|)U^\dagger\right).

Second, for every family $F_k:\mathbb C^A\to\mathbb C^B$ indexed by $K$ satisfying $\sum_kF_k^\dagger F_k=I_A$ , define $V_{(b,k),a}=(F_k)_{b,a}$ . Then $V^\dagger V=I_A$ , and $\operatorname{Tr}_K(VXV^\dagger)=\sum_kF_kXF_k^\dagger$ for every complex matrix $X$ on $A$ . For every positive semidefinite $\rho$ on $A$ of trace $1$ , one also has $S(V\rho V^\dagger)=S(\rho)$ , and, for every nonzero complex number $z$ , the complex dimensions of the $z$ -eigenspaces of $V\rho V^\dagger$ and $\rho$ are equal. Here pure-density matrices have entries $\beta_i\overline{\beta_j}$ , partial traces sum over discarded indices, and $S(M)=-\operatorname{Re}\operatorname{tr}(f(M))$ for $f(x)=x\log x$ applied by continuous functional calculus using natural logarithms and $\log0=0$ . The eigenspace equality includes non-eigenvalues, for which both dimensions are zero, and makes no assertion about the zero eigenspaces.

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