Universal energy fidelity bound and integer Fock attainment

Open

QAlgorithms.Papers.Independent.Intakethird100.P54.fixed_energy_fidelity

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$ .

Every normalized pure joint probe of finite mean total signal energy $N_s\ge0$ obeys

\mathcal F(\psi)\ge\mu^{2N_s}.

For each multimode occupation vector $\mathbf N$ , write $K=\sum_mN_m\in\mathbb N$ . Its Fock probe has mean signal energy $K$ and

\mathcal F(|\mathbf N\rangle)=\mu^{2K}.

It therefore attains the universal bound at every integer energy. The convention $0^0=1$ includes the vacuum and opposite ideal channel endpoints. This statement does not identify all minimizers or assert error-probability optimality.

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

/-- Universal real-energy fidelity lower bound and INTEGER-energy Fock attainment,
PDF p.6, (49)–(52). No false uniqueness assertion is included. The opposite ideal
endpoints use Real.rpow 0 0=1; no noninteger Fock occupation is postulated. -/
theorem fixed_energy_fidelity {M : ℕ} (hM : 0 < M) (c : Channels)
    (hc : ValidSplitters c) (hr : Reading c) :
    (∀ (J : ℕ) (psi : Hilbert (Occupation (Fin J) × Occupation (Fin M))) (N : ℝ),
      ‖psi‖=1 → HasSignalEnergy psi N → Real.rpow (splitterOverlap c) (2*N) ≤ outputFidelity c psi) ∧
    (∀ n : Occupation (Fin M), HasSignalEnergy (fock n) (photons n : ℝ) ∧
      outputFidelity c (fock n) = Real.rpow (splitterOverlap c) (2*(photons 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. 6, fixed-energy-fidelity

Read-back

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

Let $M\in\mathbb N$ with $M>0$ , and let two splitters have reflectances $R_b\in[0,1]$ , both phases zero, $r_b=\sqrt{R_b}$ , and $t_b=\sqrt{1-R_b}$ , satisfying $R_0\le R_1$ and $r_0\ne r_1$ . Put $o=r_0r_1+t_0t_1$ . For any $J\in\mathbb N$ , including $J=0$ , and any probe $\psi\in\ell^2(\mathbb N^J\times\mathbb N^M;\mathbb C)$ , define $p_n=\sum_i|\psi(i,n)|^2$ and $P_l=\sum_{n:\sum_m n_m=l}p_n$ . Define $L_b(n,k)=\prod_m\sqrt{\binom{n_m}{k_m}}r_b^{n_m-k_m}t_b^{k_m}$ when $k\le n$ componentwise and zero otherwise, and define the returned kernels by

\rho_b^\psi(x,y)=\sum_k g_{b,k}^\psi(x)\overline{g_{b,k}^\psi(y)}, \qquad g_{b,k}^\psi(i,p)=\psi(i,p+k)L_b(p+k,k).

Their output fidelity $F(\psi)$ is the real supremum of $|\langle z,w\rangle|^2$ over unit square-summable vectors on $(\mathbb N^J\times\mathbb N^M)\times\mathbb N$ whose respective marginals $\sum_e z(x,e)\overline{z(y,e)}$ and $\sum_e w(x,e)\overline{w(y,e)}$ equal $\rho_0^\psi,\rho_1^\psi$ ; the supremum is zero if its defining set is empty. The first assertion is that, for every such $J,\psi$ and every $N\in\mathbb R$ , if $\|\psi\|=1$ , $N\ge0$ , the sequence $l\mapsto lP_l$ is summable, and $\sum_l lP_l=N$ , then

o^{\,2N}\le F(\psi),

using real powers. The second assertion is that for every occupation vector $n\in\mathbb N^M$ , the vector $f_n$ that is $1$ at $(\varnothing,n)$ and zero elsewhere, with the idler occupation on zero modes denoted by $\varnothing$ , has nonnegative energy $|n|=\sum_m n_m$ , its weighted total-number sequence is summable with sum $|n|$ , and

F(f_n)=o^{\,2|n|}.

The zero occupation, hence energy zero, is included. Endpoint reflectances are allowed, including $R_0=0,R_1=1$ , when $o=0$ ; the real-power convention gives $0^0=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