claimroutineinferred_dep

Full sequence graph value below 3ν/4

Full sequence graph has value below 3ν/43\nu/4 on NO inputs
NO bound the retained graph is compared against
Claim·§A.1 A simple strong-left form of Unique Games·inside lemUnique Games with constant left degree and strong satisfaction

Statement (paper)

For every choice of right labels and every choice of left labels for the full sequence graph, which may depend on the entire ordered occurrence sequence, the uniform edge value (the average satisfied fraction) is at most s:=β+1h+(1−β)h2γ<3ν4s:=\beta+\frac1h+(1-\beta)h^2\gamma<\frac{3\nu}{4}, so the full sequence graph has value less than 3ν/43\nu/4 on a NO input.

In plain English

On a NO input, for any right labeling and any left labeling of the full sequence graph (even one depending on the whole ordered occurrence sequence), the average satisfied edge fraction is at most s=β+1h+(1−β)h2γs=\beta+\frac1h+(1-\beta)h^2\gamma, which is less than 3ν/43\nu/4. So the full sequence graph has value below 3ν/43\nu/4.

Why it's here

This turns the soundness bound <βγ<\beta\gamma for the tagged game into a soundness bound for the graph built from ordered occurrence sequences, where left labels may see the whole sequence. The three terms of ss correspond to a bad event of probability β\beta, a 1/h1/h loss, and a loss of at most h2γh^2\gamma otherwise. The bound feeds the NO-soundness of the retained graph, where the retained part is compared to this full graph.
Classified routine:
A soundness calculation for a degree-reduction/sequence-graph construction in the style of standard Unique Games preprocessing (e.g. Khot–Regev style left-degree reduction). It follows from the tagged-game soundness claim via a bad-event/averaging argument.

Uses

claimTagged right copies preserve value

Used by

claimNO soundness of the retained graph

Sources

PaperOpen
Section
§A.1 A simple strong-left form of Unique Games
Page
—
Label
—
Line
appendices/finite-consequences.tex:142
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Full sequence graph value below 3nu/4" rests on claim-lem-simple-strong-left-4