Explicit Fock Chernoff optimizer and exponent

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.fock_chernoff

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 $0<R_0<R_1<1$ , and let a Fock probe have total photon number $K\in\mathbb N$ . Put $T_b=1-R_b$ , $f(s)=R_0^sR_1^{1-s}+T_0^sT_1^{1-s}$ , and

s_*=\frac{\ln[-R_1\ln(R_0/R_1)/(T_1\ln(T_0/T_1))]}{\ln[T_0R_1/(T_1R_0)]}.

Then $s_*\in[0,1]$ minimizes $f$ , $Q_s=f(s)^K$ , and

Q=f(s_*)^K=e^{-\xi_{\rm Num}K},\qquad P_e\le\frac12f(s_*)^K,\qquad\xi_{\rm Num}=-\ln f(s_*).

The per-photon gain is defined by $G=\xi_{\rm Num}/\xi_{\rm CS}$ with $\xi_{\rm CS}=(r_1-r_0)^2$ . It is not asserted to be large for all channels. At $K=0$ , $Q=1$ .

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

/-- Number-state Chernoff bound and derived optimizer, PDF p.8, (66)–(69).
The gain is a defined per-photon ratio, not a universal large-gain claim. -/
theorem fock_chernoff {M : ℕ} (hM : 0 < M) (c : Channels)
    (hc : ValidSplitters c) (hr : Reading c) (h0 : 0 < (c false).reflectance)
    (h1 : (c true).reflectance < 1) (n : Occupation (Fin M)) :
    fockOptimizer c ∈ Set.Icc (0 : ℝ) 1 ∧
    (∀ s ∈ Set.Icc (0 : ℝ) 1,
      outputChernoffAt c (fock n) s=(fockCoefficient c s)^photons n ∧
      fockCoefficient c (fockOptimizer c) ≤ fockCoefficient c s) ∧
    outputChernoff c (fock n)=(fockCoefficient c (fockOptimizer c))^photons n ∧
    outputError c (fock n) ≤ (fockCoefficient c (fockOptimizer c))^photons n/2 ∧
    (fockCoefficient c (fockOptimizer c))^photons n =
      Real.exp (-numberExponent c*(photons n : ℝ)) ∧
    exponentGain c=numberExponent c/coherentExponent c := 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-chernoff

Read-back

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

Let $M\in\mathbb N$ satisfy $M>0$ , and let $c$ consist of two splitters with reflectances $R_b\in[0,1]$ and phases $\phi_b$ , satisfying $R_0\le R_1$ , $\sqrt{R_0}e^{i\phi_0}\ne\sqrt{R_1}e^{i\phi_1}$ , $\phi_0=\phi_1=0$ , $R_0>0$ , and $R_1<1$ . Fix $n\in\mathbb N^M$ , set $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}$ for $k\le q$ , and $0$ otherwise, and $\rho_b(x,y)=\sum_kz_{b,k}(x)\overline{z_{b,k}(y)}$ , where $z_{b,k}(i,q)=|n\rangle(i,q+k)a_b(q+k,k)$ . A resolution of a kernel $H$ is $H(x,y)=\sum_a p_a u_a(x)\overline{u_a(y)}$ , with nonnegative summable weights totaling $1$ , unit $\ell^2$ vectors at positive weights, and orthogonality between distinct positive-weight vectors; zero-weight vectors are unrestricted. Put

C_s(\rho_0,\rho_1)= \sup_{\text{resolutions }(p_a,u_a),(q_b,v_b)} \sum_{a,b}f_s(p_a)f_{1-s}(q_b)|\langle u_a,v_b\rangle|^2, \qquad C(\rho_0,\rho_1)=\inf_{s\in[0,1]}C_s(\rho_0,\rho_1),

where $f_t(0)=0$ and $f_t(p)=p^t$ otherwise. Define $e(\rho_0,\rho_1)$ as the real infimum over these resolutions 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_b q_b\operatorname{Re}\langle v_b,Ev_b\rangle$ . The suprema and infima are real, with value $0$ on empty defining sets; infinite sums have value $0$ if not summable. Define the following real quantities, using real powers in $f$ :

f(s)=R_0^sR_1^{1-s}+(1-R_0)^s(1-R_1)^{1-s}, \qquad s_*= \frac{ \log\!\left( \frac{-R_1\log(R_0/R_1)} {(1-R_1)\log((1-R_0)/(1-R_1))} \right)} {\log\!\left(\frac{(1-R_0)R_1}{(1-R_1)R_0}\right)}, \qquad \nu=-\log f(s_*), \qquad d=(\sqrt{R_1}-\sqrt{R_0})^2.

The assertion is that $s_*\in[0,1]$ , that every $s\in[0,1]$ satisfies

C_s(\rho_0,\rho_1)=f(s)^K, \qquad f(s_*)\le f(s),

and that

C(\rho_0,\rho_1)=f(s_*)^K,\qquad e(\rho_0,\rho_1)\le\frac{f(s_*)^K}{2},\qquad f(s_*)^K=e^{-\nu K}.

It also asserts that the quantity named exponent gain, whose definition is the ratio of the number exponent $\nu$ to the coherent exponent $d$ , equals $\nu/d$ . The occupation vector $n=0$ is allowed, so $K=0$ is included and the powers with exponent $K$ then equal $1$ ; no uniqueness of $s_*$ is asserted.

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