Optimal Fock photon counting and total-count threshold

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.fock_counting

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 a multimode Fock input $|\mathbf N\rangle$ with total photon number $K$ , the returned states are diagonal and commute. The observed occupation $\mathbf j$ has conditional law

\Pr_b(\mathbf j)=\prod_m\binom{N_m}{j_m}R_b^{j_m}(1-R_b)^{N_m-j_m},\quad0\le j_m\le N_m,

and zero otherwise. Its total $T=\sum_mj_m$ has the binomial law $B_b(T)=\binom KT R_b^T(1-R_b)^{K-T}$ . Photon counting followed by the likelihood decision, assigning equality to one, attains

P_e=\frac12\sum_{T=0}^K\min\{B_0(T),B_1(T)\}.

For $0<R_0<R_1<1$ and possible counts $T\le K$ , the likelihood ratio is at least one exactly when

T\ge K\frac{\ln[(1-R_0)/(1-R_1)]}{\ln[R_1(1-R_0)/(R_0(1-R_1))]}.

The optimum depends only on $K$ , independently of occupations and mode count; $K=0$ gives a tie and error $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

/-- Photon counting is optimal and depends only on total Fock photon number,
PDF p.8, (62)–(65). j counts observed photons, whereas source k counts losses.
The logarithmic likelihood rule is restricted to strict interior reflectances. -/
theorem fock_counting {M : ℕ} (hM : 0 < M) (c : Channels)
    (hc : ValidSplitters c) (hr : Reading c) (n : Occupation (Fin M)) :
    (∀ b x y, returned (c b) (fock n) x y =
      if x=y then (countLaw (c b) n x.2 : ℂ) else 0) ∧
    kernelProduct (returned (c false) (fock n)) (returned (c true) (fock n)) =
      kernelProduct (returned (c true) (fock n)) (returned (c false) (fock n)) ∧
    (∀ b j, (∑' q : Occupation (Fin M), if photons q=j then countLaw (c b) n q else 0) =
      totalCountLaw (c b) (photons n) j) ∧
    outputError c (fock n) = countingError c (photons n) ∧
    (∃ E, IsOpticalEffect E ∧ CountsAs E (fun q => decide
      (totalCountLaw (c false) (photons n) (photons q) ≤
        totalCountLaw (c true) (photons n) (photons q))) ∧
      sectorRisk c (fock n) E (1/2) (1/2)=outputError c (fock n)) ∧
    (0 < (c false).reflectance → (c true).reflectance < 1 →
      ∀ j : ℕ, j ≤ photons n →
        ((1 ≤ ((c true).reflectance^j * (1-(c true).reflectance)^(photons n-j)) /
          ((c false).reflectance^j * (1-(c false).reflectance)^(photons n-j))) ↔
        countThreshold c (photons n) ≤ (j : ℝ))) := 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. 8, fock-counting

Read-back

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

Let $M>0$ be a natural number, let $c$ specify splitters with reflectances $R_b\in[0,1]$ and phases $\phi_b$ , and 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$ . Fix $n\in\mathbb N^M$ , put $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)$ , whose idler label set is a singleton. 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}$ for $k\le q$ , and $0$ otherwise; put $z_{b,k}(i,q)=|n\rangle(i,q+k)a_b(q+k,k)$ , and $\rho_b(x,y)=\sum_kz_{b,k}(x)\overline{z_{b,k}(y)}$ . Let $s_{b,k}$ be the coefficient function $z_{b,k}$ as an $\ell^2$ vector if square summable, and the zero vector otherwise. For $q\in\mathbb N^M$ and $j\in\mathbb N$ , set

p_b(q)= \begin{cases} \displaystyle\prod_m\binom{n_m}{q_m}R_b^{q_m}(1-R_b)^{n_m-q_m},&q\le n,\\ 0,&\text{otherwise}, \end{cases} \qquad B_b(K,j)= \begin{cases} \displaystyle\binom KjR_b^j(1-R_b)^{K-j},&j\le K,\\ 0,&j>K. \end{cases}

A resolution of a kernel $H$ means $H(x,y)=\sum_a w_a u_a(x)\overline{u_a(y)}$ , with nonnegative summable weights totaling $1$ , unit $\ell^2$ vectors at positive weights, and orthogonality for distinct positive-weight vectors; 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 $(w_a,u_a),(v_a,h_a)$ and effects of $\frac12\sum_a w_a(1-\operatorname{Re}\langle u_a,Eu_a\rangle)+\frac12\sum_a v_a\operatorname{Re}\langle h_a,Eh_a\rangle$ , with empty defining set assigned infimum $0$ . The assertion is that $\rho_b(x,y)=p_b(x_{\mathrm s})$ when $x=y$ , and $0$ otherwise, for every $b,x,y$ ; that the kernel products commute, meaning

\sum_z\rho_0(x,z)\rho_1(z,y)=\sum_z\rho_1(x,z)\rho_0(z,y) \quad\text{for every }x,y; \qquad \sum_{q:\,\sum_mq_m=j}p_b(q)=B_b(K,j) \quad\text{for every }b,j;

and that

e(\rho_0,\rho_1)=\frac12\sum_{j=0}^{K}\min\{B_0(K,j),B_1(K,j)\}.

There also exists an effect $E$ such that, for every vector $v$ and label $(i,q)$ , $(Ev)(i,q)=0$ if $B_0(K,\sum_mq_m)\le B_1(K,\sum_mq_m)$ , 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).

Finally, if $R_0>0$ and $R_1<1$ , then every $j\in\mathbb N$ with $j\le K$ satisfies

1\le\frac{R_1^j(1-R_1)^{K-j}}{R_0^j(1-R_0)^{K-j}} \quad\Longleftrightarrow\quad \frac{K\log((1-R_0)/(1-R_1))} {\log\!\left(R_1(1-R_0)/(R_0(1-R_1))\right)} \le j.

The vector $n=0$ , hence $K=0$ , is included; all zeroth powers, including $0^0$ , equal $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