Universal signal-energy lower bound on discrimination error

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.error_lower_bound

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$ .

For every normalized pure joint probe with finite mean total signal photon number $N_s\ge0$ ,

P_e(\psi)\ge\frac{1-\sqrt{1-\mu^{2N_s}}}{2}.

This is a universal lower bound, independent of the numbers of signal and idler modes. At $N_s=0$ both returned states coincide, giving $P_e=1/2$ .

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

/-- Universal operational error LOWER bound, PDF pp.6–7, (53). N is the finite
mean total SIGNAL photon number, and can be zero or noninteger. -/
theorem error_lower_bound {M J : ℕ} (hM : 0 < M) (c : Channels)
    (hc : ValidSplitters c) (hr : Reading c) (psi : Hilbert (Occupation (Fin J) × Occupation (Fin M)))
    (hpsi : ‖psi‖=1) (N : ℝ) (hN : HasSignalEnergy psi N) :
    lowerError (Real.rpow (splitterOverlap c) (2*N)) ≤ outputError 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. 6, error-lower-bound

Read-back

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

Let $M,J$ be natural numbers with $M>0$ , and let $c$ specify two splitters, indexed by $b=0,1$ , with reflectances $R_b\in[0,1]$ and phases $\phi_b\in\mathbb R$ . Assume $R_0\le R_1$ , $\sqrt{R_0}e^{i\phi_0}\ne\sqrt{R_1}e^{i\phi_1}$ , and $\phi_0=\phi_1=0$ . Write $r_b=\sqrt{R_b}$ , $t_b=\sqrt{1-R_b}$ , and $o=r_0r_1+t_0t_1$ . For an occupation vector $q\in\mathbb N^M$ , put $|q|=\sum_m q_m$ . Let $\psi\in\ell^2(\mathbb N^J\times\mathbb N^M;\mathbb C)$ have norm $1$ , and let $N\in\mathbb R$ satisfy $N\ge0$ , summability of $n\mapsto nP_n$ , and $\sum_{n=0}^\infty nP_n=N$ , where $p_q=\sum_{i\in\mathbb N^J}|\psi(i,q)|^2$ and $P_n=\sum_{q:\,|q|=n}p_q$ . Define

a_b(q,k)= \begin{cases} \displaystyle\prod_{m=1}^M \sqrt{\binom{q_m}{k_m}}\,r_b^{\,q_m-k_m}t_b^{\,k_m}, &k_m\le q_m\text{ for every }m,\\ 0,&\text{otherwise}, \end{cases} \qquad z_{b,k}(i,q)=\psi(i,q+k)a_b(q+k,k), \qquad K_b(x,y)=\sum_{k\in\mathbb N^M}z_{b,k}(x)\overline{z_{b,k}(y)}.

Here and below an infinite sum is the total infinite sum, equal to $0$ if its family is not summable. For a kernel $K$ on a label set $X$ , a resolution consists of nonnegative summable weights $p_a$ of total mass $1$ and vectors $u_a\in\ell^2(X;\mathbb C)$ , with $\|u_a\|=1$ whenever $p_a>0$ , with $u_a\perp u_{a'}$ whenever $a\ne a'$ and both weights are positive, and with $K(x,y)=\sum_a p_a u_a(x)\overline{u_a(y)}$ ; zero-weight vectors have no normalization or orthogonality requirement. An effect is a bounded complex-linear operator $E$ satisfying $\langle u,Ev\rangle=\overline{\langle v,Eu\rangle}$ and $0\le\operatorname{Re}\langle v,Ev\rangle\le\|v\|^2$ for all $u,v$ . Define $e(K_0,K_1)$ as the real infimum, over resolutions $(p_a,u_a)$ and $(q_a,v_a)$ of the respective kernels and all such effects, of

\frac12\sum_a p_a\bigl(1-\operatorname{Re}\langle u_a,Eu_a\rangle\bigr) +\frac12\sum_a q_a\operatorname{Re}\langle v_a,Ev_a\rangle.

This real infimum is $0$ if its defining set is empty. The assertion is

\frac{1-\sqrt{\,1-o^{\,2N}\,}}2\le e(K_0,K_1),

where $o^{2N}$ is the real power. The hypotheses allow $J=0$ , $N=0$ , and the endpoint pair $R_0=0,R_1=1$ ; in particular, a zero base with zero exponent has value $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