One round from a correct pair reproduces the full target law

Open

QAlgorithms.Papers.Independent.Intakethird100.P78.round_correct_pair_distribution

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

prove2quantum

Let $d>2$ , let $f$ be the target permutation at fixed inputs, and fix $(\hat a,\hat b)$ satisfying $f(\hat a)=\hat b$ . Run the same one-round protocol with an independent shared coin of retention probability $1/d$ and an exact corrected smaller resource. Then, for every $a,b\in[d]$ ,

\Pr[A=a,B=b\mid\hat a,\hat b]=\begin{cases}1/d,&f(a)=b,\\0,&f(a)\ne b.\end{cases}

Thus one correct starting pair produces the full uniform graph distribution, including its uniform marginals. This result uses the disclosed correction to equation (7); independent moderation remains 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 pp.6–7, Lemma 3: a fixed correct starting pair gives the full
uniform target law in one round, not merely a matching pair almost surely.
Uses the corrected deletion-and-splicing construction (7).
Independent source-correction moderation is pending. -/
theorem round_correct_pair_distribution
    {m : ℕ} (hm : 1 < m) (f : Equiv.Perm (Fin (m + 1)))
    (ahat bhat : Fin (m + 1)) (hgood : f ahat = bhat) :
    ∀ a b, roundKernel (lt_trans Nat.zero_lt_one hm) f ahat bhat a b =
      (if f a = b then 1 / ((m + 1 : ℕ) : ℝ) else 0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P78

end

Source

Bipartite Units of Non-Locality, arXiv:0808.0651v4, PDF p. 6, Lemma 3: one round from a correct pair reproduces the full target law

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)=\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. With indicators taking values zero or one, define

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

Then for every $a,b\in I_{m+1}$ ,

W(a,b)= \begin{cases} \dfrac{1}{m+1},&f(a)=b,\\ 0,&f(a)\ne b. \end{cases}

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