Corollary 15: vanishing Renyi conditional information characterizes short quantum Markov chains

Open

QAlgorithms.Papers.Independent.Intakethird100.P52.markov_renyi

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

prove2quantum

All Hilbert spaces below are finite dimensional and nonzero over $\mathbb C$ . A density operator is positive semidefinite with trace one. Every spectral power is zero on the kernel, including zero and negative powers. Information quantities use base-two logarithms, with $\log_2 0=-\infty$ ; the operator logarithms in exponential formulas are natural logarithms.

Let $\rho$ be a density operator on $H$ , let $\sigma\ge0$ be an operator on $H$ without a trace constraint, and let $\mathcal N:\mathcal B(H)\to\mathcal B(K)$ be CPTP. Its adjoint $\mathcal N^\dagger$ is the Hilbert–Schmidt adjoint. Write

\begin{aligned} K_a&=\sigma^{(1-a)/2}\mathcal N^\dagger\!\left(\mathcal N(\sigma)^{(a-1)/2}\mathcal N(\rho)^{1-a}\mathcal N(\sigma)^{(a-1)/2}\right)\sigma^{(1-a)/2},\\ L_a&=\sigma^{(1-a)/(2a)}\mathcal N^\dagger\!\left(\mathcal N(\sigma)^{(a-1)/(2a)}\mathcal N(\rho)^{(1-a)/a}\mathcal N(\sigma)^{(a-1)/(2a)}\right)\sigma^{(1-a)/(2a)},\\ R_a&=K_a^{1/(1-a)},\qquad S_a=L_a^{a/(1-a)},\\ \Delta_a&=\frac{\log_2\operatorname{Tr}(\rho^aK_a)}{a-1},\qquad \widetilde\Delta_a=\frac{\log_2\operatorname{Tr}[(\rho^{1/2}L_a\rho^{1/2})^a]}{a-1}. \end{aligned}

Let $\rho=\rho_{ABC}$ be a tripartite density operator. Its marginals $\rho_{AC},\rho_{BC},\rho_C$ are computed by partial trace from this same state. Operators on fewer registers are extended by identities. Use tensor order $A\otimes(C\otimes B)$ , and set $\sigma=\rho_{AC}\otimes I_B$ and $\mathcal N=\operatorname{Tr}_A$ . Define $I_a(A;B\mid C)_\rho=\Delta_a(\rho,\sigma,\mathcal N)$ and $\widetilde I_a(A;B\mid C)_\rho=\widetilde\Delta_a(\rho,\sigma,\mathcal N)$ . A short quantum Markov chain $A-C-B$ means that the whole space $H_C$ decomposes as $\bigoplus_j H_{C_{L,j}}\otimes H_{C_{R,j}}$ and $\rho=\bigoplus_j q_j\rho_{AC_{L,j}}\otimes\rho_{C_{R,j}B}$ , where $q_j\ge0$ , $\sum_jq_j=1$ , and both factors in each block are density operators.

Assume $\rho_{ABC}>0$ . If $\rho$ is a short quantum Markov chain $A-C-B$ , then

I_a(A;B\mid C)_\rho=\widetilde I_a(A;B\mid C)_\rho=0 \quad\text{for every }a\in(0,1)\cup(1,\infty).

Conversely, either $I_a(A;B\mid C)_\rho=0$ for some $a\in(0,1)\cup(1,2)$ or $\widetilde I_a(A;B\mid C)_\rho=0$ for some $a\in(1/2,1)\cup(1,\infty)$ implies the Markov property.

This gives the Rényi zero-information characterization of short quantum Markov chains.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P52

Formal statement

noncomputable section

open scoped Matrix ComplexOrder

namespace QAlgorithms.Papers.Independent.Intakethird100.P52

attribute [local instance] Classical.propDecidable Classical.decEq

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

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

open QAlgorithms.Papers.Independent.Dependency50.P35 (tr elog maxRelative)

open QAlgorithms.Papers.Independent.Information100.P71 (supportPower)

open QAlgorithms.Papers.Independent.Renew46.P35 (HasMarkovBlocks)

/-- Corollary 15, PDF p.17. Positive definite tripartite densities;
HasMarkovBlocks describes the entire conditioning register C. -/
theorem markov_renyi {A C B : Type} [Fintype A] [Fintype C] [Fintype B]
    [DecidableEq A] [DecidableEq C] [DecidableEq B]
    [Nonempty A] [Nonempty C] [Nonempty B]
    (rho : Mat (A × (C × B))) (hrho : IsDensityMatrix rho)
    (hrhoPD : rho.PosDef) :
    (HasMarkovBlocks rho → ∀ a : ℝ, (0 < a ∧ a < 1) ∨ 1 < a →
      conditionalRenyiInformation a rho = 0 ∧ conditionalRenyiTilde a rho = 0) ∧
    (((∃ a : ℝ, ((0 < a ∧ a < 1) ∨ (1 < a ∧ a < 2)) ∧ conditionalRenyiInformation a rho = 0) ∨
      (∃ a : ℝ, ((1 / 2 < a ∧ a < 1) ∨ 1 < a) ∧ conditionalRenyiTilde a rho = 0)) →
      HasMarkovBlocks rho) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P52

end

Source

Quantum Markov chains, sufficiency of quantum channels, and Renyi information measures, arXiv:1501.05636v4, PDF p. 17, Corollary 15: vanishing Renyi conditional information characterizes short quantum Markov chains

Read-back

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

Let $A,C,B$ be finite, nonempty index types with decidable equality, and let $\rho$ be a positive definite complex matrix on $A\times(C\times B)$ that is positive semidefinite and has trace $1$ . Write $\rho_{AC}=\operatorname{Tr}_B\rho$ , $\sigma=\rho_{AC}\otimes I_B$ , $N=\operatorname{Tr}_A$ , $R=N(\rho)$ , and $S=N(\sigma)$ , where partial traces sum diagonal entries over the indicated register. For a positive semidefinite matrix $X$ , write $X^{[t]}$ for spectral functional calculus with scalar function $x\mapsto x^t$ for $x\ne0$ and value $0$ at $x=0$ , including when $t=0$ ; write $\operatorname{tr}X=\operatorname{Re}\operatorname{Tr}X$ , and let $\ell(x)=\log_2x$ when $x>0$ and $\ell(x)=-\infty$ otherwise. Define

\begin{aligned} K_a&=\sigma^{[(1-a)/2]} \bigl(I_A\otimes[S^{[(a-1)/2]}R^{[1-a]}S^{[(a-1)/2]}]\bigr) \sigma^{[(1-a)/2]},\\ \widetilde K_a&=\sigma^{[(1-a)/(2a)]} \bigl(I_A\otimes[S^{[(a-1)/(2a)]}R^{[(1-a)/a]}S^{[(a-1)/(2a)]}]\bigr) \sigma^{[(1-a)/(2a)]},\\ D_a&=\frac{1}{a-1}\,\ell\!\left(\operatorname{tr}(\rho^{[a]}K_a)\right),\\ \widetilde D_a&=\frac{1}{a-1}\,\ell\!\left( \operatorname{tr}\bigl((\rho^{[1/2]}\widetilde K_a\rho^{[1/2]})^{[a]}\bigr)\right). \end{aligned}

Here $D_a,\widetilde D_a$ take values in the extended real numbers. Say that $\rho$ has the stated block decomposition if there are a positive integer $r$ , positive integers $l_j,r_j$ , a unitary identification $C\cong\bigoplus_{j=1}^{r}(\mathbb C^{l_j}\otimes\mathbb C^{r_j})$ with inclusions $V_j$ , nonnegative weights $q_j$ summing to $1$ , and positive semidefinite trace-one matrices $\alpha_j$ on $A\times\{1,\ldots,l_j\}$ and $\beta_j$ on $\{1,\ldots,r_j\}\times B$ , such that

\rho=\sum_{j=1}^{r}q_j\, (I_A\otimes V_j\otimes I_B)(\alpha_j\otimes\beta_j) (I_A\otimes V_j\otimes I_B)^\dagger.

Zero weights are permitted. The declaration asserts both that this decomposition implies $D_a=\widetilde D_a=0$ for every real $a\in(0,1)\cup(1,\infty)$ , and that the decomposition exists whenever either $D_a=0$ for some $a\in(0,1)\cup(1,2)$ , or $\widetilde D_a=0$ for some $a\in(1/2,1)\cup(1,\infty)$ .

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