NDS fidelity as the squared sum of sector overlap magnitudes

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.nds_fidelity

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

prove2quantum

Let $M\ge1$ be the finite number of signal modes and $J\ge0$ the finite number of retained idler modes, on the full optical Fock spaces. The two channels have equal priors, independent vacuum environments, reflectances $0\le R_0\le R_1\le1$ , field magnitudes $r_b=\sqrt{R_b}$ and $t_b=\sqrt{1-R_b}$ , and distinct complex reflection coefficients $r_b e^{i\theta_b}$ . Every signal mode sees the same channel; idlers are retained losslessly and environment outputs are inaccessible. Write $\mathcal F$ for squared Uhlmann fidelity, $P_e$ for minimum average error over all joint binary receivers, $Q_s=\operatorname{Tr}(\rho_0^s\rho_1^{1-s})$ , and $Q=\min_{0\le s\le1}Q_s$ , with zero powers interpreted as support projections.

For a normalized pure NDS probe with multimode signal law $p_{\mathbf n}$ , use the source amplitudes $A_{\mathbf n;\mathbf k}^{(b)}=\prod_m\sqrt{\binom{n_m}{k_m}}e^{in_m\theta_b}r_b^{n_m-k_m}t_b^{k_m}$ when $\mathbf k\le\mathbf n$ , and zero otherwise. The overlap series and its outer absolute-value sum converge, and

I_{\mathbf k}=\sum_{\mathbf n}p_{\mathbf n}\overline{A_{\mathbf n;\mathbf k}^{(0)}}A_{\mathbf n;\mathbf k}^{(1)},\qquad \mathcal F=\left(\sum_{\mathbf k}|I_{\mathbf k}|\right)^2\ge\left|\sum_{\mathbf k}I_{\mathbf k}\right|^2=O(\psi).

This exact formula can improve the general bound, with equality permitted even when the channel phases differ.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P54

Formal statement

noncomputable section

open scoped BigOperators ComplexConjugate

open MeasureTheory Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P54

open QAlgorithms.RealRegisters (Hilbert)

open QAlgorithms.Papers.Independent.Claimed50.P47 (Occupation)

open QAlgorithms.Papers.Independent.Dependency50.P39 (coherentCoefficient)

attribute [local instance] Classical.propDecidable

attribute [local instance] Classical.decEq

/-- NDS fidelity with inner absolute values and a squared outer sum, PDF pp.5–6,
(30)–(31),(43)–(44). Comparison with the general bound is non-strict. -/
theorem nds_fidelity {M J : ℕ} (hM : 0 < M) (c : Channels) (hc : ValidSplitters c)
    (psi : Hilbert (Occupation (Fin J) × Occupation (Fin M))) (hpsi : ‖psi‖ = 1)
    (hnds : IsNDS psi) :
    (∀ k, Summable (lossOverlapTerm c psi k) ∧
      lossOverlap c psi k = ∑' n, lossOverlapTerm c psi k n) ∧
    Summable (fun k => ‖lossOverlap c psi k‖) ∧
    Summable (lossOverlap c psi) ∧
    outputFidelity c psi = (∑' k, ‖lossOverlap c psi k‖)^2 ∧
    Complex.normSq (∑' k, lossOverlap c psi k) = purificationOverlap c psi ∧
    purificationOverlap c psi ≤ outputFidelity c psi := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P54

end

Source

Discriminating quantum-optical beam-splitter channels with number-diagonal signal states: Applications to quantum reading and target detection, arXiv:1105.4063v3, PDF p. 5, nds-fidelity

Read-back

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

Let $M,J\in\mathbb N$ , with $M>0$ and $J$ possibly zero, and let $\psi\in\ell^2(\mathbb N^J\times\mathbb N^M;\mathbb C)$ have norm $1$ and satisfy $\sum_i\psi(i,n)\overline{\psi(i,q)}=0$ for all distinct signal occupations $n,q$ . Let two splitters have reflectances $R_b\in[0,1]$ , phases $\theta_b$ , $r_b=\sqrt{R_b}$ , and $t_b=\sqrt{1-R_b}$ , with $R_0\le R_1$ and $r_0e^{i\theta_0}\ne r_1e^{i\theta_1}$ . Define $p_n=\sum_i|\psi(i,n)|^2$ , $P_N=\sum_{n:\sum_m n_m=N}p_n$ , and $L_b(n,k)=\prod_m\sqrt{\binom{n_m}{k_m}}e^{in_m\theta_b}r_b^{n_m-k_m}t_b^{k_m}$ for $k\le n$ , with value zero otherwise. Put $g_{b,k}(i,p)=\psi(i,p+k)L_b(p+k,k)$ , and let $v_{b,k}$ be $g_{b,k}$ as a square-summable vector when possible, and zero otherwise. Set

C_k=\langle v_{0,k},v_{1,k}\rangle,\qquad T_{k,n}=p_n\overline{L_0(n,k)}L_1(n,k),\qquad U=\left|\sum_{N=0}^\infty P_Ne^{iN(\theta_1-\theta_0)} (r_0r_1+t_0t_1)^N\right|^2.

The returned kernels are $\rho_b(x,y)=\sum_k g_{b,k}(x)\overline{g_{b,k}(y)}$ , and their output fidelity $F$ is the real supremum of $|\langle z,w\rangle|^2$ over unit vectors $z,w\in\ell^2((\mathbb N^J\times\mathbb N^M)\times\mathbb N;\mathbb C)$ whose respective marginals $\sum_e z(x,e)\overline{z(y,e)}$ and $\sum_e w(x,e)\overline{w(y,e)}$ equal $\rho_0,\rho_1$ ; an empty defining set gives supremum $0$ . The theorem states that, for every $k$ , $n\mapsto T_{k,n}$ is summable and $C_k=\sum_nT_{k,n}$ ; that both $k\mapsto|C_k|$ and $k\mapsto C_k$ are summable; and that

F=\left(\sum_k|C_k|\right)^2,\qquad \left|\sum_k C_k\right|^2=U,\qquad U\le F.

All occupation indices include zero occupations, and the splitter reflectances may be endpoints.

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