claimroutineinferred_dep

YES and NO values of the final game

Final game has value ≥ 1−ε1-\varepsilon if satisfiable, ≤ δ\delta otherwise
completes the gap analysis of the theorem
Claim·§7.2 The final reduction·inside thmThe Unique Games Theorem

Statement (paper)

Let BB be the unweighted simple bipartite game obtained from the matrix game HH by Lemma  with τ\tau, and let G=B⊗tG=B^{\otimes t}. If φ\varphi is satisfiable, then val⁡(G)≥1−t(d+τ)4≥1−ε0/2≥1−ε\val(G)\ge1-\frac{t(d+\tau)}4\ge1-\eps_0/2\ge1-\eps. If φ\varphi is unsatisfiable, then val⁡(G)≤δ0≤δ\val(G)\le\delta_0\le\delta.

In plain English

For the unweighted simple bipartite game BB obtained from the matrix game HH by subdivision, and G=B⊗tG=B^{\otimes t}: if φ\varphi is satisfiable then val⁡(G)≥1−ε\val(G)\ge 1-\eps, and if φ\varphi is unsatisfiable then val⁡(G)≤δ\val(G)\le\delta.

Why it's here

This is the last step of the proof of the main theorem: it joins the parity gap, the matrix-game gap and the subdivision lemma with parallel repetition. In the satisfiable case, the loss kξ+p∗/2k\xi+p_*/2 in HH is cut by the subdivision factor and then multiplied by at most tt under repetition, and the choices of kk and ξ\xi keep the total within ε0/2\eps_0/2. In the unsatisfiable case, val⁡(H)≤99/100\val(H)\le 99/100 gives a fixed gap in BB, so tt repetitions drive the value below δ0\delta_0 by the alphabet-independent repetition bound.
Classified routine:
Direct bookkeeping that combines the earlier nodes: the matrix-game gap (prop-matrix-gap), the subdivision lemma and the parameter choices, together with the parallel repetition bound (thm-repetition). Completeness follows from a union bound over the t coordinates, and soundness from the fixed gap that claim-thm-ugc-1 supplies.

Uses

thmGap hardness for weighted parity equationslemPreprocessing to distinct variable positionspropMatrix game completeness and soundness gaplemSubdivision yields unweighted simple gamethmParallel repetition for projection gamesclaimAlphabet-independent gap fixes repetition exponentclaimChoosing the cube k and parity error

Used by

Nothing in the paper

Sources

PaperOpen
Section
§7.2 The final reduction
Page
—
Label
—
Line
sections/06-finish.tex:176
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "YES and NO values of the final game" rests on thm:repetition
  • info
    inferred_dep
    outline: "YES and NO values of the final game" rests on claim-thm-ugc-1
  • info
    inferred_dep
    outline: "YES and NO values of the final game" rests on claim-thm-ugc-3