§VI: exact noiseless-dimension converse

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.noiseless_dimension_converse

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

prove2quantum

All systems have finite positive dimension and fixed computational bases. Matrix order is Loewner order and logarithms are base two.

Let $\mathcal N:A\to B$ be CPTP and let $m_1,m_2\ge1$ be integers. Suppose $\mathcal N$ exactly simulates $\mathrm{id}_{m_1}$ with NS assistance, and $\mathrm{id}_{m_2}$ exactly simulates $\mathcal N$ with NS assistance. Then

m_1\le m_2.

Exact simulation means minimum half-diamond error zero. No nonzero-error version is asserted; this is the noiseless-dimension converse in the discussion.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P65

Formal statement

noncomputable section

open Filter QAlgorithms

open scoped BigOperators Matrix ComplexConjugate ComplexOrder Topology

namespace QAlgorithms.Papers.Independent.Intakethird100.P65

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Dependency50.P09 (transposeBob)

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

open QAlgorithms.Papers.Independent.Independent2.P01 (dampingKraus damping)

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

open QAlgorithms.Papers.Independent.Information100.P06 (Below)

open QAlgorithms.Papers.Independent.Information100.P34 (choi)

open QAlgorithms.Papers.Independent.Information100.P62 (Stochastic)

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

open QAlgorithms.Papers.Independent.Information100.P67 (IsSubnormalized purifiedDistance)

open QAlgorithms.Papers.Independent.Information100.P69 (replacer permute)

open QAlgorithms.Papers.Independent.Information100.P71 (diamond channelPower channelRelative)

open QAlgorithms.Papers.Independent.Support50.P39 (quantumMutualInformation)

variable {A B C D R : Type} [Fintype A] [DecidableEq A]
  [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C]
  [Fintype D] [DecidableEq D] [Fintype R] [DecidableEq R]

variable [Nonempty A] [Nonempty B] [Nonempty C] [Nonempty D] [Nonempty R]

/-- Section VI, exact noiseless-dimension converse, PDF p.15.
Both simulations use NS assistance and exact error zero. -/
theorem noiseless_dimension_converse (N : Superop A B) (hN : IsChannel N)
    (m1 m2 : ℕ) (h1 : 0 < m1) (h2 : 0 < m2)
    (hforward : minimumError .ns N (fun X : Mat (Fin m1) => X) = 0)
    (hbackward : minimumError .ns (fun X : Mat (Fin m2) => X) N = 0) :
    m1 ≤ m2 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P65

end

Source

Quantum Channel Simulation and the Channel's Smooth Max-Information, arXiv:1807.05354v2, PDF p. 15, §VI: exact noiseless-dimension converse

Read-back

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

For finite index types $A,B$ , equipped with decidable equality, let $N$ be a channel from complex matrices on $A$ to complex matrices on $B$ , meaning that $N(X)=\sum_jK_jXK_j^\dagger$ for every $X$ , for some finite Kraus family satisfying $\sum_jK_j^\dagger K_j=I$ . For maps $T:I\to J$ and $V:K\to L$ , define $\mathcal E_{\mathrm{NS}}(T,V)$ as the real infimum of the errors $\Delta(W_T(Q),V)$ over all channels $Q:K\times J\to I\times L$ for which there exist channels $F:K\to I$ and $G:J\to L$ satisfying $\operatorname{Tr}_LQ(X)=F(\operatorname{Tr}_JX)$ and $\operatorname{Tr}_IQ(X)=G(\operatorname{Tr}_KX)$ for every input matrix $X$ , where

W_T(Q)(X)_{\ell,\ell'}= \sum_{i,i'\in I}\sum_{j,j'\in J} T(E_{ii'})_{j,j'}\,Q(X\otimes E_{jj'})_{(i,\ell),(i',\ell')}, \qquad \Delta(S,V)=\frac12\sup_{\|X\|_1\le1} \bigl\|(\operatorname{id}_K\otimes(S-V))(X)\bigr\|_1.

Here the supremum ranges over all complex matrices $X$ on $K\times K$ , without positivity or trace-one requirements; the amplified map applies $S-V$ to each block indexed by the reference register $K$ , and $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . For every pair of positive natural numbers $m_1,m_2$ , including dimension one, if

\mathcal E_{\mathrm{NS}}(N,\operatorname{id}_{m_1})=0 \quad\text{and}\quad \mathcal E_{\mathrm{NS}}(\operatorname{id}_{m_2},N)=0,

where $\operatorname{id}_m$ is the identity map on $m\times m$ complex matrices, then $m_1\le m_2$ . The two hypotheses assert that these infima equal zero; they do not explicitly require an admissible operation attaining zero error.

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