Remark 2 / Eq.(27): input independence at full rank

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.fullRank_input_independence

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, with $A$ a reference copy of $A'$ . Let $|\psi\rangle_{AA'}$ be a unit vector whose input marginal is positive definite. With $\Phi_{AA'}$ the normalized maximally entangled state,

I_{\max}(\mathcal N)=I_{\max}(A:B)_{(\mathrm{id}_A\otimes\mathcal N)(|\psi\rangle\langle\psi|)}.

The left side is defined using $\Phi$ . Thus every full-rank purified input gives the same channel max-information. The claim is not extended to rank-deficient input marginals.

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]

/-- Remark 2, Eq.(27), PDF p.8: full rank is essential. The reference is a
copy of the input; any normalized pure purification is allowed. -/
theorem fullRank_input_independence (N : Superop A B) (hN : IsChannel N)
    (psi : EuclideanSpace ℂ (A × A)) (hpsi : ‖psi‖ = 1)
    (hfull : (traceLeft (pureDensity psi)).PosDef) :
    (channelInfo N : EReal) = maxInfo (idTensorSuperop N (pureDensity psi)) := 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. 8, Remark 2 / Eq.(27): input independence at full rank

Read-back

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

For finite index types $A,B$ , with decidable equality, let $N:A\to B$ have a finite Kraus representation with $\sum_iK_i^\dagger K_i=I_A$ . Let $\psi\in\mathbb C^{A\times A}$ have Euclidean norm $1$ , and assume the matrix $\rho_{a,a'}=\sum_r\psi(r,a)\overline{\psi(r,a')}$ is positive definite. For a vector $v$ , write $|v\rangle\langle v|_{x,y}=v_x\overline{v_y}$ ; for a matrix $X$ on $A\times A$ , define $((\mathrm{id}_A\otimes N)(X))_{(r,b),(s,b')}=N((X_{(r,a),(s,a')})_{a,a'})_{b,b'}$ . Define

D_{\max}(R\|S) =\inf\{\lambda\in\mathbb R:2^\lambda S-R\ge0\} \quad\text{in }\overline{\mathbb R},\qquad I_{\max}(R) =\inf_{\substack{\sigma\ge0\\\operatorname{tr}\sigma=1}} D_{\max}(R\|(\operatorname{Tr}_B R)\otimes\sigma).

Let $\Phi_A$ have entry $|A|^{-1}$ when both its row and column pairs have equal coordinates, and entry $0$ otherwise, and set $I(N)=(I_{\max}((\mathrm{id}_A\otimes N)(\Phi_A)))_{\mathrm{toReal}}$ , where conversion of either extended-real infinity is $0$ . Then, as an equality in the extended reals,

(I(N):\overline{\mathbb R}) =I_{\max}\bigl((\mathrm{id}_A\otimes N)(|\psi\rangle\langle\psi|)\bigr).

Thus the hypothesis concerns the second marginal of $|\psi\rangle\langle\psi|$ , with no specified value for that marginal beyond positive definiteness.

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