NDS exact discrimination and optimal loss-sector receiver

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.nds_discrimination

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.

Let the normalized pure probe be NDS: its signal marginal is diagonal in the multimode occupation basis. For each lost occupation string $\mathbf k$ , let $v_{b,\mathbf k}$ be the unnormalized retained vector constructed by the vacuum splitter, $p_{b,\mathbf k}=\|v_{b,\mathbf k}\|^2$ , $I_{\mathbf k}=\langle v_{0,\mathbf k},v_{1,\mathbf k}\rangle$ , and $H_{\mathbf k}=\operatorname{span}\{v_{0,\mathbf k},v_{1,\mathbf k}\}$ . These blocks are mutually orthogonal and have dimension at most two. Moreover $p_{b,\mathbf k}=\sum_{\mathbf n}p_{\mathbf n}|A_{\mathbf n;\mathbf k}^{(b)}|^2$ , with a convergent sum and $A=0$ unless $\mathbf k\le\mathbf n$ componentwise. Then $|I_{\mathbf k}|^2\le p_{0,\mathbf k}p_{1,\mathbf k}$ , and the convergent exact-error formula is

P_e=\frac12-\frac14\sum_{\mathbf k}\sqrt{(p_{0,\mathbf k}+p_{1,\mathbf k})^2-4|I_{\mathbf k}|^2}.

An attaining projective receiver first resolves the orthogonal loss blocks and then decides zero on the positive spectrum of $|v_{0,\mathbf k}\rangle\langle v_{0,\mathbf k}|-|v_{1,\mathbf k}\rangle\langle v_{1,\mathbf k}|$ and one on its negative spectrum. Zero eigenspaces admit arbitrary projective ties; the complement of all blocks has probability zero. For priors $\pi_b\ge0$ with $\pi_0+\pi_1=1$ , the same blocks support the weighted spectral receiver and $P_e=(1-\|\pi_0\rho_0-\pi_1\rho_1\|_1)/2$ .

The block receiver specifies an abstract optimum even in degenerate sectors, without dividing by a zero sector probability.

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

/-- Exact NDS discrimination and an attaining complete block receiver, PDF pp.4–5,
(25)–(42), and [22], p.13. Blocks have dimension AT MOST two; zero eigenvalues
are assigned arbitrary projective ties, correcting the source's degenerate-block prose. -/
theorem nds_discrimination {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, Module.Finite ℂ (lossBlock c psi k) ∧
      Module.finrank ℂ (lossBlock c psi k) ≤ 2) ∧
    (∀ k l, k ≠ l → ∀ u ∈ lossBlock c psi k, ∀ v ∈ lossBlock c psi l,
      inner ℂ u v = 0) ∧
    (∀ b k, Summable (fun n => signalLaw psi n * Complex.normSq (lossAmplitude (c b) n k)) ∧
      lossProbability c psi b k = ∑' n, signalLaw psi n * Complex.normSq (lossAmplitude (c b) n k)) ∧
    (∀ k, Complex.normSq (lossOverlap c psi k) ≤
      lossProbability c psi false k * lossProbability c psi true k) ∧
    Summable (fun k => Real.sqrt ((lossProbability c psi false k +
      lossProbability c psi true k)^2 - 4*Complex.normSq (lossOverlap c psi k))) ∧
    outputError c psi = 1/2 - (1/4) * ∑' k,
      Real.sqrt ((lossProbability c psi false k + lossProbability c psi true k)^2 -
        4*Complex.normSq (lossOverlap c psi k)) ∧
    (∃ E, BlockReceiver c psi 1 1 E ∧
      sectorRisk c psi E (1/2) (1/2) = outputError c psi) ∧
    (∀ v : Hilbert (Occupation (Fin J) × Occupation (Fin M)),
      (∀ k, ∀ w ∈ lossBlock c psi k, inner ℂ w v = 0) →
      ∀ b, (∑' k, Complex.normSq (inner ℂ (lossSector (c b) psi k) v)) = 0) ∧
    (∀ pi0 pi1 : ℝ, 0 ≤ pi0 → 0 ≤ pi1 → pi0+pi1=1 →
      bayesError (returned (c false) psi) (returned (c true) psi) pi0 pi1 =
        (1-weightedTraceNorm (returned (c false) psi) (returned (c true) psi) pi0 pi1)/2 ∧
      ∃ E, BlockReceiver c psi pi0 pi1 E ∧
        sectorRisk c psi E pi0 pi1 =
          bayesError (returned (c false) psi) (returned (c true) psi) pi0 pi1) := 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-discrimination

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$ , and let $\psi\in H=\ell^2(\mathbb N^J\times\mathbb N^M;\mathbb C)$ have norm $1$ . Let two splitters have reflectances $R_b\in[0,1]$ , phases $\theta_b\in\mathbb R$ , $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}$ . Assume that

\sum_i\psi(i,n)\overline{\psi(i,q)}=0 \quad\text{whenever }n,q\in\mathbb N^M,\ n\ne q.

Define $p_n=\sum_i|\psi(i,n)|^2$ 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}$ when $k\le n$ componentwise, and $L_b(n,k)=0$ otherwise. Put $g_{b,k}(i,p)=\psi(i,p+k)L_b(p+k,k)$ , let $v_{b,k}\in H$ be this function if it is square-summable and the zero vector otherwise, and put

\rho_b(x,y)=\sum_k g_{b,k}(x)\overline{g_{b,k}(y)},\quad P_{b,k}=\|v_{b,k}\|^2,\quad C_k=\langle v_{0,k},v_{1,k}\rangle,\quad H_k=\operatorname{span}_{\mathbb C}\{v_{0,k},v_{1,k}\}.

For clarity, a resolution $(a_n,u_n)$ of a kernel $K$ means summable weights $a_n\ge0$ of sum $1$ , vectors $u_n\in H$ that are unit whenever $a_n>0$ and mutually orthogonal at distinct positive weights, and $K(x,y)=\sum_n a_nu_n(x)\overline{u_n(y)}$ ; zero-weight vectors are unrestricted. An effect is a bounded complex-linear $E:H\to H$ with $\langle u,Ev\rangle=\overline{\langle v,Eu\rangle}$ and $0\le q_E(v)\le\|v\|^2$ , where $q_E(v)=\operatorname{Re}\langle v,Ev\rangle$ . Define

B(\pi_0,\pi_1)= \inf_{(a,u),(b,w),E} \left[\pi_0\sum_n a_n(1-q_E(u_n)) +\pi_1\sum_n b_nq_E(w_n)\right],

using resolutions of $\rho_0,\rho_1$ and effects $E$ , and define

W(w_0,w_1)= \sup_{(a,u),(b,w),T} \left[w_0\sum_n a_nq_T(u_n)-w_1\sum_n b_nq_T(w_n)\right],

where $T$ is bounded and complex linear, satisfies the same self-adjointness identity, and satisfies $|q_T(v)|\le\|v\|^2$ for every $v$ . These are total real infima and suprema, with value $0$ on empty defining sets. Set $E_{\mathrm{out}}=B(1/2,1/2)$ . A block receiver with weights $w_0,w_1$ means an effect $E$ with $E^2=E$ , preserving every $H_k$ , such that, whenever $v\in H_k$ and

w_0\langle v_{0,k},v\rangle v_{0,k} -w_1\langle v_{1,k},v\rangle v_{1,k}=a v \quad(a\in\mathbb R),

one has $Ev=v$ if $a>0$ and $Ev=0$ if $a<0$ ; this condition prescribes neither choice when $a=0$ . Define its sector risk by

S_E(\pi_0,\pi_1)= \pi_0\sum_k\bigl(P_{0,k}-q_E(v_{0,k})\bigr) +\pi_1\sum_k q_E(v_{1,k}).

The theorem asserts that every $H_k$ is finite-dimensional with complex dimension at most $2$ , including dimensions $0$ and $1$ ; different $H_k$ are orthogonal; for every $b,k$ , the sequence $n\mapsto p_n|L_b(n,k)|^2$ is summable and $P_{b,k}=\sum_n p_n|L_b(n,k)|^2$ ; and $|C_k|^2\le P_{0,k}P_{1,k}$ for every $k$ . It further asserts that $k\mapsto\sqrt{(P_{0,k}+P_{1,k})^2-4|C_k|^2}$ is summable and

E_{\mathrm{out}} =\frac12-\frac14\sum_k\sqrt{(P_{0,k}+P_{1,k})^2-4|C_k|^2},

that some block receiver with weights $1,1$ satisfies $S_E(1/2,1/2)=E_{\mathrm{out}}$ , and that every $v\in H$ orthogonal to every $H_k$ satisfies $\sum_k|\langle v_{b,k},v\rangle|^2=0$ for each $b$ . Finally, for every $\pi_0,\pi_1\ge0$ with $\pi_0+\pi_1=1$ , including either prior being zero,

B(\pi_0,\pi_1)=\frac{1-W(\pi_0,\pi_1)}2,

and there exists a block receiver with weights $\pi_0,\pi_1$ whose sector risk is $B(\pi_0,\pi_1)$ .

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