claimroutineinferred_dep

Output is simple bipartite translation game

Output

B^{\otimes t}

is a simple bipartite translation game over

\mathbb F_2^s

checks the structural requirements of the output

Claim·§7.2 The final reduction·inside thmThe Unique Games Theorem

Statement (paper)

The output

G=B^{\otimes t}

is a simple bipartite graph, with vertex sets the

t

-fold products of the two sides of

B

, and uniform edge sampling on

G

is independent uniform edge sampling in the

t

coordinates. Every constraint of

G

is a translation

a(v_e)=a(u_e)+c_e

K^t=\F_2^{\ell t}=\F_2^s

, with

s=\ell t\ge1

fixed by the prescribed errors, the translation having offset

(c_1,\ldots,c_t)

built from the translation offsets of

B

In plain English

The output game

G=B^{\otimes t}

is a simple bipartite graph on

t

-fold products of the sides of

B

, where sampling a uniform edge of

G

amounts to sampling independent uniform edges of

B

in each of the

t

coordinates. Each constraint of

G

is a translation

a(v_e)=a(u_e)+c_e

K^t=\F_2^{s}

with

s=\ell t

fixed by the target errors, and the offset is

(c_1,\ldots,c_t)

built from the offsets of

B

Why it's here

This claim checks that the tensor power keeps the structural requirements of the theorem: simplicity, bipartiteness, unweighted uniform edge sampling, and translation constraints over

\F_2^s

. It works because

B

is already an unweighted simple bipartite translation game by the subdivision lemma, and products of such edges and constraints act coordinatewise, so the properties carry over to

B^{\otimes t}

Classified routine:

Direct bookkeeping consequence of the subdivision lemma (lem-unweighted-subdivision): tensor powers of an unweighted simple bipartite translation game act coordinatewise on edges and constraints, so simplicity, bipartiteness, uniform sampling and translation form carry over.

Uses

lemSubdivision yields unweighted simple game

Used by

Nothing in the paper

Sources

PaperOpen

Section: §7.2 The final reduction
Page: —
Label: —
Line: sections/06-finish.tex:204

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Output is simple bipartite translation game" rests on lem:unweighted-subdivision