Fock optimality for the ideal-memory Chernoff coefficient

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.ideal_memory_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 $R_1=1$ . For every normalized pure joint probe, including arbitrary finite retained idlers, $\rho_1=|\psi\rangle\langle\psi|$ and

Q(\psi)=\mathcal F(\psi),\qquad P_e(\psi)\le\frac{\mathcal F(\psi)}2.

Every Fock occupation with total photon number $K\in\mathbb N$ attains $Q=R_0^K$ , which is no larger than the Chernoff coefficient of any normalized pure joint probe of mean signal energy $K$ .

This is optimality of the Chernoff bound, distinguished from a general minimum-error assertion.

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

/-- Ideal-memory Chernoff optimality for all pure idler-assisted competitors,
PDF p.7, (58). Integer-energy Fock probes attain the smallest coefficient;
no general minimum-opticalError optimality is claimed here. -/
theorem ideal_memory_chernoff {M : ℕ} (hM : 0 < M) (c : Channels)
    (hc : ValidSplitters c) (hr : Reading c) (hideal : (c true).reflectance=1) :
    (∀ (J : ℕ) (psi : Hilbert (Occupation (Fin J) × Occupation (Fin M))), ‖psi‖=1 →
      returned (c true) psi = opticalPureKernel psi ∧
      outputChernoff c psi = outputFidelity c psi ∧
      outputError c psi ≤ outputFidelity c psi/2) ∧
    (∀ n : Occupation (Fin M),
      outputChernoff c (fock n) = (c false).reflectance ^ photons n ∧
      ∀ (J : ℕ) (psi : Hilbert (Occupation (Fin J) × Occupation (Fin M))),
        ‖psi‖=1 → HasSignalEnergy psi (photons n : ℝ) →
          outputChernoff c (fock n) ≤ outputChernoff 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. 7, ideal-memory-chernoff

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$ 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$ , and $R_1=1$ . For every $J\in\mathbb N$ and every norm-one $\psi\in\ell^2(\mathbb N^J\times\mathbb N^M;\mathbb C)$ , define $a_b(q,k)$ to be $\prod_m\sqrt{\binom{q_m}{k_m}}R_b^{(q_m-k_m)/2}(1-R_b)^{k_m/2}$ when $k\le q$ , understood equivalently as integer powers of $\sqrt{R_b}$ and $\sqrt{1-R_b}$ , and $0$ otherwise; put $z_{b,k}(i,q)=\psi(i,q+k)a_b(q+k,k)$ and $K_b^\psi(x,y)=\sum_k z_{b,k}(x)\overline{z_{b,k}(y)}$ . For kernels $K,H$ on $X$ , let $F(K,H)$ be the real supremum of $|\langle z,w\rangle|^2$ over norm-one $z,w\in\ell^2(X\times\mathbb N;\mathbb C)$ satisfying $\sum_e z(x,e)\overline{z(y,e)}=K(x,y)$ and $\sum_e w(x,e)\overline{w(y,e)}=H(x,y)$ . A resolution of a kernel is a representation $K(x,y)=\sum_a p_a u_a(x)\overline{u_a(y)}$ , with nonnegative summable weights of sum $1$ , unit vectors at positive weights, and orthogonality between distinct vectors of positive weight; vectors of zero weight are unrestricted. Set

C_s(K,H)=\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(K,H)=\inf_{s\in[0,1]}C_s(K,H),

where $f_t(0)=0$ and $f_t(p)=p^t$ otherwise. Let $e(K,H)$ be the infimum, over the same 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$ . All these extrema are real, with empty defining sets assigned value $0$ , and infinite sums have value $0$ if not summable. The first assertion, with no finite-energy hypothesis on $\psi$ , is

K_1^\psi(x,y)=\psi(x)\overline{\psi(y)},\qquad C(K_0^\psi,K_1^\psi)=F(K_0^\psi,K_1^\psi),\qquad e(K_0^\psi,K_1^\psi)\le\frac{F(K_0^\psi,K_1^\psi)}2.

The second assertion is that, for every $n\in\mathbb N^M$ , writing $K=\sum_m n_m$ and letting $|n\rangle$ be the unit coordinate vector at $(0,n)$ in $\ell^2(\mathbb N^0\times\mathbb N^M;\mathbb C)$ ,

C(K_0^{|n\rangle},K_1^{|n\rangle})=R_0^K,

and this value is at most $C(K_0^\psi,K_1^\psi)$ for every $J\in\mathbb N$ and every norm-one $\psi$ for which $P_\ell=\sum_{q:\,\sum_mq_m=\ell}\sum_i|\psi(i,q)|^2$ satisfies summability of $\ell\mapsto\ell P_\ell$ and $\sum_\ell\ell P_\ell=K$ . Zero idler modes and $K=0$ are included, with $R_0^0=1$ , also when $R_0=0$ .

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