Ideal-memory EPR Chernoff endpoint

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.epr_ideal

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$ and let $M\ge1$ identical EPR pairs each have signal energy $N\ge0$ . Then

Q=\mathcal F=[1+(1-r_0)N]^{-2M},\qquad P_e\le\frac12[1+(1-r_0)N]^{-2M}.

The support endpoint $s_*=1$ attains the coefficient and is no larger than $Q_s$ for any $s\in[0,1]$ .

This formula includes the vacuum and does not evaluate the generic undefined ratio $T_0/T_1$ at $T_1=0$ .

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 EPR endpoint, PDF p.10, (90); optimizer s=1 is a conclusion.
No division by the zero ideal transmission is performed. -/
theorem epr_ideal (M : ℕ) (hM : 0 < M) (c : Channels) (hc : ValidSplitters c)
    (hr : Reading c) (h1 : (c true).reflectance=1) (N : ℝ) (hN : 0 ≤ N) :
    outputChernoff c (tmsvProbe M N)=outputFidelity c (tmsvProbe M N) ∧
    outputChernoff c (tmsvProbe M N)=((1-(c false).r)*N+1)^(-(2*M : ℤ)) ∧
    outputChernoffAt c (tmsvProbe M N) 1=outputChernoff c (tmsvProbe M N) ∧
    (∀ s ∈ Set.Icc (0 : ℝ) 1,
      outputChernoffAt c (tmsvProbe M N) 1 ≤ outputChernoffAt c (tmsvProbe M N) s) ∧
    outputError c (tmsvProbe M N) ≤ (1/2)*((1-(c false).r)*N+1)^(-(2*M : ℤ)) := 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. 10, epr-ideal

Read-back

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

Let $M$ be a positive natural number and let two splitters have reflectances $R_b\in[0,1]$ and phases $\theta_b$ , indexed by $b\in\{0,1\}$ , with $R_0\le R_1$ , $\sqrt{R_0}e^{i\theta_0}\ne\sqrt{R_1}e^{i\theta_1}$ , $\theta_0=\theta_1=0$ , and $R_1=1$ ; hence $0\le R_0<1$ . Let $N\ge0$ , set $r_b=\sqrt{R_b}$ , $t_b=\sqrt{1-R_b}$ , and define the probe $\psi$ on $\mathbb N^M\times\mathbb N^M$ by

\psi(p,n)= \begin{cases} \displaystyle\prod_{m=1}^{M}\sqrt{\frac1{N+1}} \left(\sqrt{\frac N{N+1}}\right)^{n_m},&p=n,\\ 0,&p\ne n. \end{cases}

This coefficient function is regarded as a vector in complex $\ell^2$ if it is square-summable and is replaced by zero otherwise. For $b=0,1$ , define

A_b(n,k)= \begin{cases} \displaystyle\prod_m\sqrt{\binom{n_m}{k_m}}\, r_b^{\,n_m-k_m}t_b^{\,k_m},&k\le n\text{ componentwise},\\ 0,&\text{otherwise}, \end{cases} \qquad K_b((p,n),(q,v)) =\sum_{k\in\mathbb N^M} \psi(p,n+k)A_b(n+k,k) \overline{\psi(q,v+k)A_b(v+k,k)}.

For a kernel $K$ on $X=\mathbb N^M\times\mathbb N^M$ , a resolution means weights $a_j\ge0$ forming a summable sequence of sum one and vectors $u_j\in\ell^2(X;\mathbb C)$ satisfying $K(x,y)=\sum_j a_j u_j(x)\overline{u_j(y)}$ , with $\|u_j\|=1$ whenever $a_j>0$ and $\langle u_j,u_k\rangle=0$ for distinct positive-weight indices; no normalization is required at zero weight. Set $h(a,s)=0$ when $a=0$ , and $h(a,s)=a^s$ otherwise, using real powers, and define

C_s=\sup_{\substack{(a_j,u_j)\text{ resolves }K_0\$b_j,v_j)\text{ resolves }K_1}} \sum_{j,k\ge0}h(a_j,s)h(b_k,1-s)|\langle u_j,v_k\rangle|^2, \qquad C=\inf_{s\in[0,1]}C_s.

Thus zero weights contribute zero even when their exponent is zero. Let (F $be the supremum of$ |\langle z,w\rangle|^2 $over unit vectors$ z,w\in\ell^2(X\times\mathbb N;\mathbb C) $with marginals$ \sum_e z(x,e)\overline{z(y,e)}=K_0(x,y) $and$ \sum_e w(x,e)\overline{w(y,e)}=K_1(x,y) $. Let$ P $be the infimum over the two resolutions and bounded complex-linear operators$ E=E^* $satisfying$ 0\le\operatorname{Re}\langle v,Ev\rangle\le|v|^2 $for every$ v$, of

\frac12\sum_j a_j(1-\operatorname{Re}\langle u_j,Eu_j\rangle) +\frac12\sum_j b_j\operatorname{Re}\langle v_j,Ev_j\rangle.

These definitions use real suprema and infima, assigning zero to an empty defining set. The declaration asserts

C=F,\qquad C=\bigl((1-r_0)N+1\bigr)^{-2M},\qquad C_1=C,\qquad \forall s\in[0,1],\ C_1\le C_s,\qquad P\le\frac12\bigl((1-r_0)N+1\bigr)^{-2M}.

The powers $-2M$ are integer powers; $N=0$ , $R_0=0$ , and both endpoints $s=0,1$ are included.

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