Corrected exact Fock ideal-memory error

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.fock_ideal_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_1=1$ . For any multimode Fock occupation with total signal photon number $K$ ,

P_e=\frac12R_0^K=\frac{\mathcal F}{2}=\frac Q2.

Photon counting followed by decision one exactly when the total returned count equals $K$ is optimal, including the $K=0$ tie.

Source correction. Printed equation (71) contains an extraneous $\ln$ before $1/2$ . The counting rule and the next paragraph's equality $P_e=\mathcal F/2$ force the displayed correction; the printed formula would be negative. Independent moderation of this correction remains required.

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 ideal-memory error, PDF p.9, (71)–(72). SOURCE CORRECTION:
printed (71) has an extraneous 'ln' before 1/2. It is deleted here because the
printed counting rule and the following equality Pe=F/2 force R0^K/2; a logarithm
would make a probability negative. Preserve the printed formula in items/HARD. -/
theorem fock_ideal_error {M : ℕ} (hM : 0 < M) (c : Channels)
    (hc : ValidSplitters c) (hr : Reading c) (h1 : (c true).reflectance=1)
    (n : Occupation (Fin M)) :
    outputError c (fock n)=(c false).reflectance^photons n/2 ∧
    outputError c (fock n)=outputFidelity c (fock n)/2 ∧
    outputError c (fock n)=outputChernoff c (fock n)/2 ∧
    ∃ E, IsOpticalEffect E ∧ CountsAs E (fun q => decide (photons q=photons n)) ∧
      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-ideal-error

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$ specify 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_1=1$ . 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)$ . Set $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 define $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 $s_{b,k}$ as the coefficient function $z_{b,k}$ if square summable, and as the zero $\ell^2$ vector otherwise. 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 for distinct positive-weight vectors; zero-weight vectors are unrestricted. Define $e(\rho_0,\rho_1)$ as the real infimum over resolutions $(p_a,u_a),(q_a,v_a)$ and bounded complex-linear effects $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$ . Define $F(\rho_0,\rho_1)$ as the real supremum of $|\langle z,w\rangle|^2$ over norm-one $z,w\in\ell^2(X\times\mathbb N;\mathbb C)$ , where $X=\mathbb N^0\times\mathbb N^M$ , whose marginals $\sum_ez(x,e)\overline{z(y,e)}$ and $\sum_ew(x,e)\overline{w(y,e)}$ equal $\rho_0,\rho_1$ , respectively. Finally put

C(\rho_0,\rho_1)= \inf_{s\in[0,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,

where $f_t(0)=0$ and $f_t(p)=p^t$ otherwise. All extrema are real, with value $0$ for empty defining sets, and infinite sums have value $0$ if not summable. The assertion is

e(\rho_0,\rho_1)=\frac{R_0^K}{2} =\frac{F(\rho_0,\rho_1)}2 =\frac{C(\rho_0,\rho_1)}2,

and there exists an effect $E$ such that, for every vector $v$ and label $(i,q)$ , $(Ev)(i,q)=0$ if $\sum_mq_m=K$ , 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 hypotheses allow $R_0=0$ and $n=0$ ; every zeroth power, including $0^0$ , is $1$ .

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