Forward classical assistance is characterized by regularized formation

Open

QAlgorithms.Papers.Independent.Intakethird100.P27.classical_assistance_formation

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

prove2quantum

Fix a finite-dimensional memoryless source $\rho_A$ , a unit purification $\psi_{RA}$ with $R\simeq A$ , a finite nonempty reconstruction register $B$ , and a positive observable $\Delta_{RB}$ . For $D\ge0$ , let $R^q_{\to}(D)$ be the infimum of asymptotically achievable quantum communication rates using unlimited noiseless forward classical communication and no prior entanglement. The encoder is a quantum instrument with quantum message $W$ and classical message $M$ ; Bob applies an $M$ -conditioned CPTP decoder. The quantum cost per block is $\log_2\dim W$ .

For any block channel $\mathcal N^{(k)}:A^k\to B^k$ , put $\omega^{(k)}=(\mathrm{id}_{R^k}\otimes\mathcal N^{(k)})(\psi^{\otimes k})$ , and let $\bar d$ be its average single-letter observable distortion. Then

R^q_{\to}(D)=\lim_{k\to\infty}\frac1k\min_{\mathcal N^{(k)}:\bar d\le D}E_F(\omega^{(k)}).

The limit exists, and each nonempty feasible positive-block channel set has an attaining minimizer. $E_F$ is entanglement of formation across $R^k:B^k$ , in bits. If distortion is infeasible, the infimum convention gives infinity on both sides.

This realizes the abstract's formation characterization in the general observable-distortion model.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P27

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P27

open Filter

open scoped Matrix ComplexConjugate ComplexOrder ENNReal

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Dependency50.P19
  (first marginalRB mutualInformation bipartiteBlock epr)

open QAlgorithms.Papers.Independent.Information100.P08 (formation)

open QAlgorithms.Papers.Independent.Gap48.P20 (redistributionMarginal)

open QAlgorithms.Papers.Independent.Bridge50.P37 (isotropicState normalizedEntangledProjection)

/-- PDF pp.6--8, Theorem 10, realizing the abstract seed on p.1: convergence to
the independently operational forward-classically-assisted rate, together with
attainment of every feasible positive-block outer minimum. No limit, entropy
identity, or optimizing channel is assumed. Below feasibility the values are infinity. -/
theorem classical_assistance_formation {A B : Type} [Fintype A] [Fintype B]
    [Nonempty A] [Nonempty B] (S : DistortionSource A B) (D : ℝ) (hD : 0 ≤ D) :
    Tendsto (fun k => formationBlockValue S D (k + 1)) atTop
      (nhds (rateDistortion S .classical D)) ∧
    (∀ k : ℕ, 1 ≤ k →
      (∃ N : Superop (IidRegister A k) (IidRegister B k), IsChannel N ∧
        averageDistortion S (iidChannelOutput S k N) ≤ D) →
      ∃ N : Superop (IidRegister A k) (IidRegister B k), IsChannel N ∧
        averageDistortion S (iidChannelOutput S k N) ≤ D ∧
        ∀ M : Superop (IidRegister A k) (IidRegister B k), IsChannel M →
          averageDistortion S (iidChannelOutput S k M) ≤ D →
            formation (iidChannelOutput S k N) ≤ formation (iidChannelOutput S k M)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P27

end

Source

Quantum rate distortion coding with auxiliary resources, arXiv:1212.5316v3, PDF p. 6, Theorem 10; abstract seed p.1

Read-back

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

Let $A,B$ be finite nonempty types, let $S$ consist of a unit vector $\psi\in\mathbb C^{A\times A}$ and a positive semidefinite matrix $\Delta$ on $A\times B$ , and let $D\ge0$ . For $k\ge1$ , let $\mathcal F_k$ be the set of channels $N$ from matrices on $A^k$ to matrices on $B^k$ for which $\bar d_S(X_N)\le D$ , where

X_N((a,b),(a',b')) = N\!\left( \left(\prod_{i<k}\psi(a_i,x_i)\overline{\psi(a'_i,y_i)}\right)_{x,y} \right)(b,b'), \qquad \bar d_S(X)=\frac1k\sum_{i<k}\operatorname{Re}\operatorname{Tr}(\Delta X_i),

and $X_i$ is the partial trace over all positions other than $i$ , obtained by summing equal row and column indices there. Every channel mentioned here must have a finite Kraus representation with $\sum_jK_j^\dagger K_j=I$ . Define $E_F(X)$ as the real infimum of $\sum_jp_jS_2(H_j)$ over finite decompositions $X=\sum_jp_ju_ju_j^\dagger$ , where $p_j\ge0$ , $\sum_jp_j=1$ , $\|u_j\|=1$ , $H_j(a,a')=\sum_bu_j(a,b)\overline{u_j(a',b)}$ , and $S_2(H)=-\operatorname{Re}\operatorname{Tr}((x\mapsto x\log_2x)(H))$ , with $0\log_2 0=0$ ; an empty defining set gives real infimum $0$ . Put

b_k=\frac1k\inf_{N\in\mathcal F_k}\max(E_F(X_N),0) \quad\text{in }[0,\infty],

with empty constrained infimum $+\infty$ . Let $R_{\rm cl}$ be the infimum in $[0,\infty]$ of all nonnegative real $r$ such that, for every $\varepsilon,s>0$ , every sufficiently large positive $n$ admits positive integers $c,q$ , a channel encoder $A^n\to\operatorname{Fin}(c)\times\operatorname{Fin}(q)$ , and a channel decoder $\operatorname{Fin}(c)\times\operatorname{Fin}(q)\to B^n$ , with the encoder output block diagonal between distinct classical labels for every input matrix, such that $\log_2q\le n(r+s)$ and the output on the second halves of $n$ copies of $\psi$ has average distortion at most $D+\varepsilon$ . These codes have only a one-dimensional shared register, and their classical dimension $c$ is unrestricted. The theorem asserts both

b_{k+1}\longrightarrow R_{\rm cl}\quad(k\to\infty)

in $[0,\infty]$ , and that for every $k\ge1$ , if $\mathcal F_k$ is nonempty, there exists $N\in\mathcal F_k$ satisfying $E_F(X_N)\le E_F(X_M)$ for every $M\in\mathcal F_k$ . No existence of a feasible channel is asserted for an individual block length.

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