One round from a fixed incorrect pair has error exactly two over d

Open

QAlgorithms.Papers.Independent.Intakethird100.P78.round_incorrect_pair_error

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $d>2$ and let $f$ be the target permutation at a fixed input pair. Fix starting labels $(\hat a,\hat b)$ with $f(\hat a)\ne\hat b$ . Draw a fresh shared coin, independently of an exact copy of the corrected smaller resource from Lemma 1. With probability $1/d$ retain the starting pair; otherwise query the resource at the augmented local inputs and relabel its two outputs with $r_{\hat a}$ and $r_{\hat b}$ .

If $(A,B)$ is the resulting pair, then

\Pr[f(A)\ne B\mid\hat a,\hat b]=\frac{2}{d}.

The equality describes the error of a single round conditioned on its fixed initial pair. It uses the disclosed correction to equation (7), whose independent moderation is pending.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P78

Formal statement

noncomputable section

open scoped BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P78

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF p.6, Lemma 2: conditional on a fixed incorrect initial pair, the
round's mismatch probability equals 2/d. This uses corrected (7), as
disclosed above; it does not assume the conclusion that Dprime is a permutation.
Independent source-correction moderation is pending. -/
theorem round_incorrect_pair_error
    {m : ℕ} (hm : 1 < m) (f : Equiv.Perm (Fin (m + 1)))
    (ahat bhat : Fin (m + 1)) (hbad : f ahat ≠ bhat) :
    (∑ a, ∑ b, if f a ≠ b then
      roundKernel (lt_trans Nat.zero_lt_one hm) f ahat bhat a b else 0) =
        2 / ((m + 1 : ℕ) : ℝ) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P78

end

Source

Bipartite Units of Non-Locality, arXiv:0808.0651v4, PDF p. 6, Lemma 2: one round from an incorrect pair has error probability 2/d

Read-back

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

Let $m\in\mathbb N$ satisfy $1<m$ , let $f$ be a permutation of $I_{m+1}=\{0,\ldots,m\}$ , and let $\alpha,\beta\in I_{m+1}$ satisfy $f(\alpha)\ne\beta$ . Put $I_m=\{0,\ldots,m-1\}$ , let $S_h$ exchange $h$ and $m$ , and define $L_h(u)=S_h(u)$ for $u\in I_m$ and $D_h(v)=S_h(v)\bmod m$ for $v\in I_{m+1}$ . Define $r(u)=D_\beta(f(\alpha))$ if $f(L_\alpha(u))=\beta$ , and $r(u)=D_\beta(f(L_\alpha(u)))$ otherwise. For $a,b\in I_{m+1}$ , define the real-valued array

W(a,b)= \frac{\mathbf 1_{\{a=\alpha,\ b=\beta\}}}{m+1} +\frac{m}{m+1} \sum_{u\in I_m}\sum_{v\in I_m} \frac{\mathbf 1_{\{L_\alpha(u)=a,\ L_\beta(v)=b,\ r(u)=v\}}}{m},

where an indicator is one when its condition holds and zero otherwise. Then the sum of $W(a,b)$ over all pairs $a,b\in I_{m+1}$ satisfying $f(a)\ne b$ is exactly

\sum_{\substack{a,b\in I_{m+1}\\f(a)\ne b}}W(a,b)=\frac{2}{m+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