Exact Fock target-detection error

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.fock_target_error

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$ . For any multimode Fock occupation with total signal photon number $K$ ,

P_e=\frac12(1-R_1)^K.

Photon counting with decision 'present' exactly when the total returned count is positive attains this error. At $K=0$ it always declares absence and has error $1/2$ ; at $R_1=1$ and $K>0$ the error is zero.

This gives an exact endpoint rule without a logarithmic threshold.

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 Fock target-detection error and attaining count>0 rule, PDF p.9, (70).
K=0 is a tie with opticalError 1/2; the endpoint R1=1 is included. -/
theorem fock_target_error {M : ℕ} (hM : 0 < M) (c : Channels)
    (hc : ValidSplitters c) (hr : Reading c) (h0 : (c false).reflectance=0)
    (n : Occupation (Fin M)) :
    outputError c (fock n)=(1-(c true).reflectance)^photons n/2 ∧
    ∃ E, IsOpticalEffect E ∧ CountsAs E (fun q => decide (0 < photons q)) ∧
      sectorRisk c (fock n) E (1/2) (1/2)=outputError c (fock n) := 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. 9, fock-target-error

Read-back

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

Let $M>0$ be a natural number, and let $c$ give two splitters with reflectances $R_b\in[0,1]$ and phases $\phi_b$ , satisfying $R_0\le R_1$ , unequal fields $\sqrt{R_0}e^{i\phi_0}\ne\sqrt{R_1}e^{i\phi_1}$ , $\phi_0=\phi_1=0$ , and $R_0=0$ . Fix $n\in\mathbb N^M$ , let $K=\sum_mn_m$ , and let $|n\rangle$ be the unit coordinate vector at $(0,n)$ in $\ell^2(\mathbb N^0\times\mathbb N^M;\mathbb C)$ . Define $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$ , and $0$ otherwise; set $z_{b,k}(i,q)=|n\rangle(i,q+k)a_b(q+k,k)$ , $\rho_b(x,y)=\sum_kz_{b,k}(x)\overline{z_{b,k}(y)}$ , and let $s_{b,k}$ be $z_{b,k}$ as an $\ell^2$ vector if square summable, and $0$ otherwise. A resolution of a kernel $H$ is $H(x,y)=\sum_a p_a u_a(x)\overline{u_a(y)}$ , where the weights are nonnegative and summable with sum $1$ , each vector with positive weight is unit, and distinct positive-weight vectors are orthogonal; zero-weight vectors are unrestricted. An effect is a bounded complex-linear operator $E$ with $\langle u,Ev\rangle=\overline{\langle v,Eu\rangle}$ and $0\le\operatorname{Re}\langle v,Ev\rangle\le\|v\|^2$ . Let $e(\rho_0,\rho_1)$ be the real infimum, over resolutions $(p_a,u_a),(q_a,v_a)$ and effects, 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$ , with empty defining set assigned value $0$ . Then

e(\rho_0,\rho_1)=\frac{(1-R_1)^K}{2},

and there exists an effect $E$ such that every vector $v$ satisfies $(Ev)(i,q)=0$ when $\sum_mq_m>0$ , and $(Ev)(i,q)=v(i,q)$ otherwise, and such that

\frac12\sum_k\left(\|s_{0,k}\|^2-\operatorname{Re}\langle s_{0,k},Es_{0,k}\rangle\right) +\frac12\sum_k\operatorname{Re}\langle s_{1,k},Es_{1,k}\rangle =e(\rho_0,\rho_1).

The case $n=0$ , hence $K=0$ , and the endpoint $R_1=1$ are included, with $0^0=1$ ; infinite sums have value $0$ if not summable.

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