The corrected smaller resource is a permutation system

Proved

QAlgorithms.Papers.Independent.Intakethird100.P78.reduced_resource_is_permutation

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

prove2quantum

Let $X$ and $Y$ be finite nonempty input alphabets, let $d>2$ , and for every $(x,y)$ let $f^{xy}$ be a permutation of $[d]=\{1,\ldots,d\}$ . The target permutation system assigns mass $1/d$ to each pair $(a,f^{xy}(a))$ .

For a deleted label $h$ , let $r_h:[d-1]\to[d]\setminus\{h\}$ replace $h$ by $d$ and leave all other labels fixed. Define the corrected smaller map, for $u=r_{\hat a}(a)$ , by

f'^{(x,\hat a)(y,\hat b)}(a)=r_{\hat b}^{-1}\!\left(\begin{cases}f^{xy}(\hat a),&f^{xy}(u)=\hat b,\\f^{xy}(u),&f^{xy}(u)\ne\hat b.\end{cases}\right).

The graph law of these maps, with mass $1/(d-1)$ , belongs to $\mathcal D$ : every smaller map is a permutation and its output size is greater than one. Its local input alphabets are $X\times[d]$ and $Y\times[d]$ .

This is the alphabet-reduction step used in the bipartite simulation construction. The condition in printed equation (7) is corrected as described in the audit; independent moderation of this source correction 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 pp.4–5, Lemma 1 (corrected construction): Dprime belongs to D.
Printed (7) is changed to test f(r_ahat(a)) = bhat before splicing; the
printed condition can map a surviving edge to the deleted output.
The reduction is restricted to d = m+1 > 2, because D excludes size 1.
Independent source-correction moderation is pending. -/
theorem reduced_resource_is_permutation
    {X Y : Type} [Fintype X] [Fintype Y] [Nonempty X] [Nonempty Y]
    {m : ℕ} (hm : 1 < m)
    (F : X → Y → Equiv.Perm (Fin (m + 1))) :
    IsPermutationSystem (reducedKernel (lt_trans Nat.zero_lt_one hm) F) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P78

end

Source

Bipartite Units of Non-Locality, arXiv:0808.0651v4, PDF p. 4, Lemma 1: the reduced resource is a permutation system (corrected construction)

Read-back

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

Let $X$ and $Y$ be finite, nonempty types, let $m\in\mathbb N$ satisfy $1<m$ , and, for every $x\in X$ and $y\in Y$ , let $F_{x,y}$ be a permutation of $I_{m+1}=\{0,\ldots,m\}$ . Write $I_m=\{0,\ldots,m-1\}$ . For $h\in I_{m+1}$ , let $S_h$ exchange $h$ and $m$ , fixing all other labels; define $L_h(u)=S_h(u)$ for $u\in I_m$ , using its natural inclusion in $I_{m+1}$ , and $D_h(v)=S_h(v)\bmod m$ for $v\in I_{m+1}$ . For $\alpha,\beta\in I_{m+1}$ , define

r_{x,y,\alpha,\beta}(u) = D_\beta\!\left( \begin{cases} F_{x,y}(\alpha),&F_{x,y}(L_\alpha(u))=\beta,\\ F_{x,y}(L_\alpha(u)),&F_{x,y}(L_\alpha(u))\ne\beta, \end{cases}\right)

and define $K((x,\alpha),(y,\beta),u,v)$ to be $1/m$ when $r_{x,y,\alpha,\beta}(u)=v$ , and zero otherwise. The conclusion is that $1<m$ and there exists a family of maps $G_{(x,\alpha),(y,\beta)}:I_m\to I_m$ , each bijective, such that for every $x,y,\alpha,\beta,u,v$ , the value $K((x,\alpha),(y,\beta),u,v)$ equals $1/m$ when $G_{(x,\alpha),(y,\beta)}(u)=v$ , and zero otherwise.

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