claimroutineinferred_dep

Clean pairs are independent game questions

Clean pairs are independent honest questions of the game

lets clean coordinates act as game samples

Claim·§6.2 Vanishing advice on clean coordinates·inside lemAdvice agreement decays with clean coordinates

Statement (paper)

Conditional on

R=r

, for every value

r

of positive probability, the pairs

(e_i,v_{e_i,j_i})

i\in I

, where

I

is the clean set recorded in

r

, are independent question pairs of

G_{\mathcal E}

, each distributed according to the ordinary equation--variable distribution.

In plain English

Conditioned on the recorded randomness

R=r

(with clean set

I

), the pairs

(e_i,v_{e_i,j_i})

for

i\in I

are independent question pairs of

G_{\mathcal E}

, each with the ordinary equation–variable distribution.

Why it's here

Building on the previous claim, where cleanness is independent across coordinates and unbiased in the question law, this shows that conditioning on

R=r

leaves the clean coordinates' questions fresh and independent. This lets later claims treat the clean pairs as honest samples of the game, so the local strategies' agreement can be bounded by the game's value, which is at most

4/5

when

\OPT(\mathcal E)\le 4/5

Classified routine:

A direct conditioning consequence of the preceding claim (independent cleanness with unbiased question law), obtained by standard product-distribution bookkeeping, similar to the clean/ordinary coordinate arguments in parallel-repetition-style analyses.

Uses

claimClean coordinates have ordinary question law

Used by

claimEach side reconstructs its advice input

Sources

PaperOpen

Section: §6.2 Vanishing advice on clean coordinates
Page: —
Label: —
Line: sections/05-clean.tex:141

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Conditioned clean pairs are independent game questions" rests on claim-lem-clean-2