Supplement III.B, Eqs.(146)–(149): exact illumination spectrum with source corrections

Open

QAlgorithms.Papers.Independent.Intakethird100.P49.illumination_exact_spectrum

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

prove2quantum

Let $d\ge1$ be the number of single-photon modes, $D=d+1$ , $0\le b$ , $db\le1$ , and $0\le\eta\le1$ . With one photon total plus vacuum, set $\tau_b=(1-db)|0\rangle\langle0|+bI_{\rm one}$ , $\mathcal E_0(X)=\operatorname{tr}(X)\tau_b$ , and $\mathcal E_1=(1-\eta)\mathcal E_0+\eta\,\mathrm{id}$ . These are CPTP. For their normalized Choi states $\sigma,\rho$ , put $\Omega^2=\sqrt\sigma\rho\sqrt\sigma$ and $a=1-db$ . Its spectrum, including multiplicity, consists of

d^2\text{ copies of }\frac{(1-\eta)b^2}{D^2},\quad d\text{ copies of }\frac{(1-\eta)a^2}{D^2},\quad\operatorname{spec}(C/D^2),

where $C_{00}=(1-\eta)a^2+\eta a$ , $C_{0k}=C_{k0}=\eta\sqrt{ab}$ , $C_{kk}=(1-\eta)b^2+\eta b$ for $k>0$ , and $C_{jk}=\eta b$ for distinct positive $j,k$ . Thus $F(\sigma,\rho)=\sum_{\lambda\in\operatorname{spec}(\Omega^2)}\sqrt\lambda$ . The factors $1-\eta$ omitted in the printed spectrum and lower-block diagonal are restored from exact Eq. (148), pending independent correction review. This retains an exact finite illumination calculation without relying on the subsequent expansion.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P49

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P49

open QAlgorithms Filter

open scoped Matrix ComplexConjugate ComplexOrder BigOperators

attribute [local instance] Classical.propDecidable Classical.decEq

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

open QAlgorithms.Papers.Independent.Dependency50.P18 (bipartiteTensor)

open QAlgorithms.Papers.Independent.Information100.P71 (diamond AdaptiveTest adaptiveInput adaptiveAccept)

open QAlgorithms.Papers.Independent.Bridge50.P25
  (LOCCOn normalizedChannelChoi TwoWayGenerationCode TwoWayChannelProtocol
   generationCodeError twoWayGenerationCapacity sendChannelRegister StateFunctional
   IsDimensionChangingLOCCMonotone privateStateInPartyOrder)

open QAlgorithms.Papers.Independent.Support50.P07 (amplitudeDampingChannel)

/-- Supplement III.B, PDF p.17, (146)--(149): exact illumination spectrum.
Printed d^2-fold eigenvalue b^2/D^2 is changed to (1-eta)*b^2/D^2;
printed lower-block diagonal is changed as documented in illuminationBlock.
Both corrections are forced by exact (148); independent moderation is required.
Eigenvalues are a multiset, so coincidences and zero eigenvalues keep multiplicity. -/
theorem illumination_exact_spectrum (d : ℕ) (hd : 1 ≤ d) (b eta : ℝ)
    (hb : 0 ≤ b) (hdb : (d : ℝ)*b ≤ 1) (heta : eta ∈ Set.Icc 0 1) :
    IsChannel (illuminationChannel d b 0) ∧ IsChannel (illuminationChannel d b eta) ∧
    (List.ofFn (ascEigenvalues (illuminationOmegaSquared d b eta))).Perm
      (List.replicate (d*d) ((1-eta)*b^2/((d : ℝ)+1)^2) ++
       List.replicate d ((1-eta)*(1-d*b)^2/((d : ℝ)+1)^2) ++
       List.ofFn (ascEigenvalues (illuminationBlock d b eta))) ∧
    rootFidelity (normalizedChannelChoi (illuminationChannel d b 0))
      (normalizedChannelChoi (illuminationChannel d b eta)) =
      ∑ i, Real.sqrt (ascEigenvalues (illuminationOmegaSquared d b eta) i) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P49

end

Source

Fundamental limits to quantum channel discrimination, arXiv:1803.02834v4, PDF p. 17, Supplement III.B, Eqs.(146)–(149): exact illumination spectrum with source corrections

Read-back

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

For every natural number $d\ge1$ and real numbers $b,\eta$ satisfying $b\ge0$ , $db\le1$ , and $0\le\eta\le1$ , put $D=d+1$ , let $\tau=\operatorname{diag}(1-db,b,\ldots,b)$ on $\mathbb C^D$ , and define the matrix map

\mathcal N_\eta(X)=(1-\eta)\operatorname{tr}(X)\tau+\eta X.

For any such map $\mathcal N$ , write $J(\mathcal N)=(\operatorname{id}\otimes\mathcal N)(|\Phi_D\rangle\langle\Phi_D|)$ , where $\Phi_D=D^{-1/2}\sum_{i=0}^{D-1}|i,i\rangle$ ; here amplification by the identity means applying $\mathcal N$ to each block indexed by the first register. Set $\sigma=J(\mathcal N_0)$ , $\rho=J(\mathcal N_\eta)$ , and $\Omega=\sqrt{\sigma}\,\rho\,\sqrt{\sigma}$ , with matrix square roots defined by continuous functional calculus. Define the $D\times D$ matrix $B$ , indexed by $0,\ldots,d$ , by

B_{ij}=\frac1{D^2} \begin{cases} (1-\eta)(1-db)^2+\eta(1-db),&i=j=0,\\ \eta\sqrt{(1-db)b},&\text{exactly one of }i,j\text{ is }0,\\ (1-\eta)b^2+\eta b,&i=j>0,\\ \eta b,&i,j>0,\ i\ne j. \end{cases}

Then both $\mathcal N_0$ and $\mathcal N_\eta$ admit finite Kraus representations $X\mapsto\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ ; the list of ascending eigenvalues of $\Omega$ , including multiplicities, is a permutation of the concatenation of $d^2$ copies of $(1-\eta)b^2/D^2$ , $d$ copies of $(1-\eta)(1-db)^2/D^2$ , and the ascending eigenvalue list of $B$ ; and

\operatorname{Re}\operatorname{tr}\sqrt{\sqrt{\sigma}\,\rho\,\sqrt{\sigma}} =\sum_{i=0}^{D^2-1}\sqrt{\lambda_i(\Omega)}.

The ascending-eigenvalue function used here returns the Hermitian eigenvalues in ascending order, and returns the all-zero list for a non-Hermitian matrix. The hypotheses include $d=1$ , $b=0$ , $db=1$ , and both endpoints $\eta=0,1$ , so zero eigenvalues and repeated eigenvalues are included.

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