Strict finite-round total-variation bound with exact smaller resources

Open

QAlgorithms.Papers.Independent.Intakethird100.P78.finite_round_distance_bound

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

prove2quantum

Let $X,Y$ be finite nonempty input alphabets and let $D_d$ be a permutation system with $d>2$ outputs on each side. Start with independent uniform local labels in $[d]$ . Run $n\ge1$ rounds of the stated protocol using independent exact copies of the corrected resource $D'(D_d)$ and fresh shared coins, with retention probability $1/d$ in every round. Write $S_n$ for the resulting conditional output law.

With worst-input total variation defined by $\delta(S,D)=\max_{x,y}\frac12\sum_{a,b}|S(a,b\mid x,y)-D(a,b\mid x,y)|$ , one has

\delta(S_n,D_d)<\left(\frac{2}{d}\right)^n.

This estimates the error of the explicitly defined finite-round construction. The source correction to equation (7) is inherited and awaits independent moderation.

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.7, (9): positive n exact smaller-resource rounds give a strict
worst-input total-variation bound. The initial independent-uniform guess
is part of finiteRoundKernel. Uses corrected (7); independent moderation
of that source correction remains pending. -/
theorem finite_round_distance_bound
    {X Y : Type} [Fintype X] [Fintype Y] [Nonempty X] [Nonempty Y]
    {m : ℕ} (hm : 1 < m)
    (F : X → Y → Equiv.Perm (Fin (m + 1)))
    (n : ℕ) (hn : 0 < n) :
    simulationDistance
      (finiteRoundKernel (lt_trans Nat.zero_lt_one hm) F n)
      (graphKernel (fun x y => F x y)) <
        (2 / ((m + 1 : ℕ) : ℝ)) ^ n := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P78

end

Source

Bipartite Units of Non-Locality, arXiv:0808.0651v4, PDF p. 7, Unnumbered quantitative result (9): finite-round approximation using exact smaller resources

Read-back

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

Let $X,Y$ be finite, nonempty types, let $m\in\mathbb N$ satisfy $1<m$ , let $F_{x,y}$ be a permutation of $I_{m+1}=\{0,\ldots,m\}$ for each $x\in X,y\in Y$ , and let $n\in\mathbb N$ satisfy $0<n$ . Put $I_m=\{0,\ldots,m-1\}$ . For $h\in I_{m+1}$ , let $S_h$ exchange $h$ and $m$ , define $L_h(u)=S_h(u)$ for $u\in I_m$ , and define $D_h(v)=S_h(v)\bmod m$ . For any permutation $f$ of $I_{m+1}$ and $\alpha,\beta\in I_{m+1}$ , set $r_{f,\alpha,\beta}(u)=D_\beta(f(\alpha))$ if $f(L_\alpha(u))=\beta$ , and $r_{f,\alpha,\beta}(u)=D_\beta(f(L_\alpha(u)))$ otherwise, and define

W_f(\alpha,\beta;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_{f,\alpha,\beta}(u)=v\}}}{m}.

Define arrays $K_j$ recursively by $K_0(x,y,a,b)=1/(m+1)^2$ and

K_{j+1}(x,y,a,b)= \sum_{\alpha,\beta\in I_{m+1}} K_j(x,y,\alpha,\beta)\,W_{F_{x,y}}(\alpha,\beta;a,b).

Also define $H(x,y,a,b)=1/(m+1)$ when $F_{x,y}(a)=b$ , and zero otherwise. Then

\sup_{(x,y)\in X\times Y} \frac12\sum_{a,b\in I_{m+1}} \left|K_n(x,y,a,b)-H(x,y,a,b)\right| < \left(\frac{2}{m+1}\right)^n.

The bound concerns positive $n$ ; the zero-round array is included in the recursive definition but $n=0$ is excluded by the hypothesis.

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