NDS fidelity minimization at a prescribed photon law

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.nds_fidelity_minimization

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. Here the common phase is removed, so $\theta_0=\theta_1=0$ and $R_0<R_1$ . Put $\mu=r_0r_1+t_0t_1$ .

Let $|\psi\rangle$ be any normalized pure NDS probe, and let $p_n$ be its total signal photon law. Then

\mathcal F(\psi)=\left(\sum_{n=0}^\infty p_n\mu^n\right)^2\le\mathcal F(\phi)

for every normalized pure competitor $|\phi\rangle$ with the same total law, allowing any finite number of retained idler modes. In addition, every probability law on multimode signal occupations is realized by a normalized NDS purification with one freely chosen optical idler.

Thus the bound is attained at a prescribed total law, in particular when the entire multimode occupation law is fixed; no adequate purification is postulated in an arbitrarily small prescribed idler space.

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 probes minimize fidelity at fixed TOTAL signal photon law, PDF p.6, (48).
Comparators have arbitrary finite idler count. Realizability is asserted with a freely
chosen single optical idler, rather than a possibly inadequate prescribed idler. -/
theorem nds_fidelity_minimization {M J : ℕ} (hM : 0 < M) (c : Channels)
    (hc : ValidSplitters c) (hr : Reading c) (psi : Hilbert (Occupation (Fin J) × Occupation (Fin M)))
    (hpsi : ‖psi‖ = 1) (hnds : IsNDS psi) :
    outputFidelity c psi = (∑' n : ℕ, totalLaw psi n * (splitterOverlap c)^n)^2 ∧
    (∀ (Jother : ℕ) (other : Hilbert (Occupation (Fin Jother) × Occupation (Fin M))),
      ‖other‖ = 1 → totalLaw other = totalLaw psi →
        outputFidelity c psi ≤ outputFidelity c other) ∧
    (∀ p : Occupation (Fin M) → ℝ, (∀ n, 0 ≤ p n) → Summable p → (∑' n, p n)=1 →
      ∃ z : Hilbert (Occupation (Fin 1) × Occupation (Fin M)),
        ‖z‖=1 ∧ IsNDS z ∧ signalLaw z=p) := 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. 6, nds-fidelity-minimization

Read-back

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

Let $M,J\in\mathbb N$ with $M>0$ , allowing $J=0$ . Let two splitters have reflectances $R_b\in[0,1]$ , both phases equal to zero, $r_b=\sqrt{R_b}$ , and $t_b=\sqrt{1-R_b}$ , with $R_0\le R_1$ and $r_0\ne r_1$ . 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 every distinct $n,q\in\mathbb N^M$ . For any probe $\phi$ , put $p_n^\phi=\sum_i|\phi(i,n)|^2$ and $P_N^\phi=\sum_{n:\sum_mn_m=N}p_n^\phi$ . Define $L_b(n,k)=\prod_m\sqrt{\binom{n_m}{k_m}}r_b^{n_m-k_m}t_b^{k_m}$ if $k\le n$ componentwise and zero otherwise; define $g_{b,k}^\phi(i,p)=\phi(i,p+k)L_b(p+k,k)$ and $\rho_b^\phi(x,y)=\sum_k g_{b,k}^\phi(x)\overline{g_{b,k}^\phi(y)}$ . Let $F(\phi)$ be the real supremum of $|\langle z,w\rangle|^2$ over norm-one square-summable vectors on the output labels times $\mathbb N$ 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^\phi,\rho_1^\phi$ ; the supremum of an empty defining set is $0$ . With $o=r_0r_1+t_0t_1$ , the theorem asserts

F(\psi)=\left(\sum_{N=0}^{\infty}P_N^\psi o^N\right)^2.

It also asserts that, for every $J_{\mathrm{other}}\in\mathbb N$ and every norm-one $\phi\in\ell^2(\mathbb N^{J_{\mathrm{other}}}\times\mathbb N^M;\mathbb C)$ satisfying $P_N^\phi=P_N^\psi$ for every $N$ , one has $F(\psi)\le F(\phi)$ , without requiring $\phi$ to satisfy the orthogonality condition imposed on $\psi$ . Finally, for every summable function $p:\mathbb N^M\to\mathbb R$ with $p_n\ge0$ and $\sum_n p_n=1$ , there exists $z\in\ell^2(\mathbb N\times\mathbb N^M;\mathbb C)$ of norm $1$ such that $\sum_i z(i,n)\overline{z(i,q)}=0$ for all distinct $n,q$ , and $\sum_i|z(i,n)|^2=p_n$ for every $n$ . Zero occupations and endpoint reflectances 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