Monotonicity and endpoints of the ancillary-overlap lower bound

Proved

QAlgorithms.Papers.Independent.Intakenext100.P97.bound_monotonicity

by Gohan · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Fix $0\le f<1$ and positive integers $N,M$ , and set $L=N+M$ . Define the scalar function

B_{N,M}(f,\phi)=f^N\phi-\frac{f^L\sqrt{1-f^{2N}\phi^2}}{\sqrt{1-f^{2L}}}.

This function is nondecreasing on $[f^M,1]$ , and its minimum and maximum occur at the endpoints:

B_{N,M}(f,f^M)=0,\qquad 0\le B_{N,M}(f,\phi)\le B_{N,M}(f,1)\quad(f^M\le\phi\le1).

For one original and one additional copy, the maximum has the explicit value

B_{1,1}(f,1)=f-\frac{f^2}{\sqrt{1+f^2}}.

This describes the scalar lower bound as ancillary overlap varies; it makes no attainability assertion about an arbitrary device.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P97

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate

namespace QAlgorithms.Papers.Independent.Intakenext100.P97

open QAlgorithms.Papers.Independent.Information100.P67
  (squaredFidelity sineDistance receiverChannel)

open QAlgorithms.Papers.Independent.Dependency50.P48 (densityPower)

/-- PDF p.4, paragraphs after Eqs. (21) and (23). The scalar bound is
nondecreasing (constant zero for `f=0`), with the stated endpoint minimum
and maximum. This is not an attainability assertion about arbitrary cloners. -/
theorem bound_monotonicity {N M : ℕ} (hN : 1 ≤ N) (hM : 1 ≤ M)
    (f : ℝ) (hf0 : 0 ≤ f) (hf1 : f < 1) :
    MonotoneOn (cloningBound N M f) (Set.Icc (f ^ M) 1) ∧
    cloningBound N M f (f ^ M) = 0 ∧
    (∀ phi ∈ Set.Icc (f ^ M) 1,
      0 ≤ cloningBound N M f phi ∧ cloningBound N M f phi ≤ cloningBound N M f 1) ∧
    cloningBound 1 1 f 1 = standardBound f := by sorry

end QAlgorithms.Papers.Independent.Intakenext100.P97

end

Source

Lower bound on the relative error of mixed-state cloning and related operations, arXiv:quant-ph/0208159v2, PDF p. 4, §IV, paragraphs after Eqs. (21) and (23)

Read-back

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

For all natural numbers $N,M\ge 1$ and real numbers $f$ with $0\le f<1$ , define

B_{N,M,f}(\phi) =f^N\phi- \frac{f^{N+M}\sqrt{1-f^{2N}\phi^2}} {\sqrt{1-f^{2(N+M)}}}.

Then $B_{N,M,f}$ is nondecreasing on the closed interval $[f^M,1]$ : whenever $f^M\le\phi\le\psi\le1$ , one has $B_{N,M,f}(\phi)\le B_{N,M,f}(\psi)$ . Moreover,

B_{N,M,f}(f^M)=0,\qquad 0\le B_{N,M,f}(\phi)\le B_{N,M,f}(1) \quad\text{for every }\phi\in[f^M,1],

and

B_{1,1,f}(1)=f-\frac{f^2}{\sqrt{1+f^2}}.

The case $f=0$ is included; in that case $B_{N,M,0}$ is identically zero. The denominator in the definition of $B_{N,M,f}$ is positive under the stated hypotheses.

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph