Zero-background target envelopes and fixed-energy high-loss limit

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.target_detection_no_go

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

Assume $R_0=0$ and fix a finite $N_s\ge0$ . For $R=R_1$ , define

L(R,N_s)=\frac{1-\sqrt{1-(1-R)^{N_s}}}{2},\qquad C(R,N_s)=\frac{1-\sqrt{1-e^{-RN_s}}}{2}.

Every normalized pure joint probe of signal energy $N_s$ has error at least $L(R_1,N_s)$ . Every product coherent probe with that signal energy, with arbitrary pure coherent idlers, has exact error $C(R_1,N_s)$ . For each fixed $N_s$ ,

\lim_{R\downarrow0}\bigl(C(R,N_s)-L(R,N_s)\bigr)=0,\qquad\lim_{R\downarrow0}\frac{-\ln(1-R)}R=1.

These precise envelopes express the paper's high-loss comparison without a tolerance for 'appreciable' or a uniform relative-error claim at unbounded energy. The background environment is vacuum.

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 zero-background target envelopes and their fixed-energy high-loss limit,
PDF p.7, (59)–(60). The prose 'appreciable' is given no invented uniform tolerance. -/
theorem target_detection_no_go {M J : ℕ} (hM : 0 < M) (c : Channels)
    (hc : ValidSplitters c) (hr : Reading c) (habsent : (c false).reflectance=0)
    (N : ℝ) (hN : 0 ≤ N) :
    (∀ psi : Hilbert (Occupation (Fin J) × Occupation (Fin M)), ‖psi‖=1 → HasSignalEnergy psi N →
      targetLower (c true).reflectance N ≤ outputError c psi) ∧
    (∀ (beta : Fin J → ℂ) (alpha : Fin M → ℂ), coherentEnergy alpha=N →
      outputError c (coherentOpticalProbe beta alpha) = targetCoherent (c true).reflectance N) ∧
    Tendsto (fun R : ℝ => targetCoherent R N - targetLower R N)
      (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) ∧
    Tendsto (fun R : ℝ => -Real.log (1-R)/R)
      (nhdsWithin 0 (Set.Ioi 0)) (nhds 1) := 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. 7, target-detection-no-go

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 let $c$ be two splitters with reflectances $R_b\in[0,1]$ and phases $\phi_b$ , such that $R_0\le R_1$ , their fields $\sqrt{R_0}e^{i\phi_0}$ and $\sqrt{R_1}e^{i\phi_1}$ differ, $\phi_0=\phi_1=0$ , and $R_0=0$ . Let $N\in\mathbb R$ satisfy $N\ge0$ . For any probe $\chi\in\ell^2(\mathbb N^J\times\mathbb N^M;\mathbb C)$ , put $a_b(q,k)=\prod_m\sqrt{\binom{q_m}{k_m}}(\sqrt{R_b})^{q_m-k_m}(\sqrt{1-R_b})^{k_m}$ when $k\le q$ coordinatewise and $0$ otherwise, and define its returned kernel by $K_b^\chi(x,y)=\sum_k\chi(x_{\mathrm i},x_{\mathrm s}+k)a_b(x_{\mathrm s}+k,k)\overline{\chi(y_{\mathrm i},y_{\mathrm s}+k)a_b(y_{\mathrm s}+k,k)}$ . A resolution of a kernel on $X$ is $K(x,y)=\sum_a p_a u_a(x)\overline{u_a(y)}$ , with $u_a\in\ell^2(X;\mathbb C)$ , nonnegative summable weights of sum $1$ , unit vectors at positive weights, and orthogonality for distinct positive-weight vectors; zero-weight vectors are unrestricted. Write $e(K,H)$ for the real infimum over resolutions $(p_a,u_a),(q_a,v_a)$ of $K,H$ and bounded complex-linear $E$ satisfying $\langle u,Ev\rangle=\overline{\langle v,Eu\rangle}$ and $0\le\operatorname{Re}\langle v,Ev\rangle\le\|v\|^2$ , of $\frac12\sum_a p_a(1-\operatorname{Re}\langle u_a,Eu_a\rangle)+\frac12\sum_a q_a\operatorname{Re}\langle v_a,Ev_a\rangle$ ; the empty defining set has infimum $0$ . First, for every norm-one $\psi$ such that $P_n=\sum_{q:\,\sum_mq_m=n}\sum_i|\psi(i,q)|^2$ has $n\mapsto nP_n$ summable and $\sum_n nP_n=N$ ,

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

Second, for every $\beta\in\mathbb C^J$ and $\alpha\in\mathbb C^M$ with $\sum_m|\alpha_m|^2=N$ , define $h_z(n)=e^{-|z|^2/2}z^n/\sqrt{n!}$ , and let $\psi_{\beta,\alpha}$ be the coefficient function $(i,q)\mapsto\prod_jh_{\beta_j}(i_j)\prod_mh_{\alpha_m}(q_m)$ as an $\ell^2$ vector if square summable, and $0$ otherwise. Then

e(K_0^{\psi_{\beta,\alpha}},K_1^{\psi_{\beta,\alpha}}) =\frac{1-\sqrt{\,1-e^{-R_1N}\,}}2.

Finally, the following two right-hand limits hold:

\lim_{R\to0^+} \left(\frac{1-\sqrt{\,1-e^{-RN}\,}}2- \frac{1-\sqrt{\,1-(1-R)^N\,}}2\right)=0, \qquad \lim_{R\to0^+}\frac{-\log(1-R)}R=1.

Here real powers are used, the limits range over real $R>0$ approaching $0$ , and all infinite sums are total sums, equal to $0$ if not summable. The statement permits $J=0$ , $N=0$ , and $R_1=1$ ; in particular $0^0=1$ in the real power.

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