claimroutineinferred_dep

Pseudorandom vertices have local payoff bound

Pseudorandom vertices have payoff ≤ opt⁡q(J)\operatorname{opt}_q(J) plus small errors
local bound for pseudorandom vertices
Claim·§A.2 The finite ordering transfer·inside propFinite ordering transfer from Unique Games

Statement (paper)

For every left vertex a∈Aa\in A that is pseudorandom at threshold tt, Va(O)≤Sloc:=opt⁡q(J)+(k2)(q−κ/2+q rc(t))+rs(kqt).V_a(O)\le S_{\mathrm{loc}}:=\operatorname{opt}_q(J)+\binom{k}{2}\bigl(q^{-\kappa/2}+q\,r_c(t)\bigr)+r_s(kqt).

In plain English

For every left vertex aa that is pseudorandom at threshold tt, its payoff Va(O)V_a(O) under the ordering OO is at most Sloc=opt⁡q(J)+(k2)(q−κ/2+q rc(t))+rs(kqt)S_{\mathrm{loc}}=\operatorname{opt}_q(J)+\binom{k}{2}(q^{-\kappa/2}+q\,r_c(t))+r_s(kqt).

Why it's here

This bounds the contribution of pseudorandom left vertices by a uniform local constant. The block functions are simplex-valued, have mean 1/q1/q and low influence, so the rounding lemma gives the opt⁡q(J)+rs(kqt)\operatorname{opt}_q(J)+r_s(kqt) term and the collision lemma controls pairs of ordering coordinates, giving the (k2)(q−κ/2+q rc(t))\binom{k}{2}(q^{-\kappa/2}+q\,r_c(t)) term. The next claim then shows that if the total payoff exceeds this bound, nonpseudorandom vertices must account for the excess, which decodes to a good game labeling.
Classified routine:
Direct combination of the earlier rounding lemma (giving the opt_q(J)+r_s(kqt) term) and the collision lemma applied to pairs of ordering coordinates, using the simplex-valued, low-influence block functions from the previous claim; this is the standard soundness step in Raghavendra/Guruswami et al.-style ordering-CSP reductions from Unique Games.

Uses

lemLow-influence functions cannot beat opt_q(J)lemLow-influence functions rarely collide under couplingclaimBlock functions are simplex-valued, low influence

Used by

claimNonpseudorandom excess decodes to game labeling

Sources

PaperOpen
Section
§A.2 The finite ordering transfer
Page
—
Label
—
Line
appendices/finite-consequences.tex:737
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Pseudorandom vertices have local payoff bound" rests on claim-prop-finite-ordering-transfer-2