claimroutineinferred_dep

Conditional agreement bounded by repeated game

Given

R=r

, agreement is at most the

|I|

-fold repeated game value

applies parallel repetition to the clean coordinates

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

Statement (paper)

For every value

r

of the conditioning randomness

R

(with clean index set

I

\Pr[\bar\pi a_U=a_O\mid R=r]\le \val(G_{\mathcal E}^{\otimes\abs{I}})\le \left(1-\frac{1}{3600}\right)^{\abs{I}}

, where the right-hand side is interpreted as one when

I=\varnothing

In plain English

Conditioned on any value

r

of the recorded randomness

R

, with clean index set

I

, the probability that the strategies' outputs agree,

\bar\pi a_U=a_O

, is at most the value of the

|I|

-fold repetition of the game

G_{\mathcal E}

, which is at most

(1-1/3600)^{|I|}

(taken as one if

I

is empty).

Why it's here

Given

R=r

, the previous claim makes each side's advice input a function of

r

and its own question, so the two local strategies become a strategy for the repeated game

G_{\mathcal E}^{\otimes|I|}

on the independent clean coordinates. Since

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

gives a constant gap, the parallel repetition theorem yields the exponential decay in

|I|

, and the next claim averages this bound over the random size of

I

(binomial).

Classified routine:

Follows directly from the previous claim (advice is determined by r and each side's own question) by viewing the local strategies as a strategy for the repeated game, then applying the parallel repetition bound for projection games with gap 1/5, since (1/5)^2/16 = 1/400 and 1/400 ≥ 1/3600.

Uses

thmParallel repetition for projection gamesclaimEach side reconstructs its advice input

Used by

claimAveraging over binomial clean count

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Conditional agreement bounded by repeated game" rests on claim-lem-clean-4