claimroutineinferred_dep

Polynomial-time explicit encoding

The reduction is deterministic polynomial time with an explicit encoding
running-time part of the theorem
Claim·§7.2 The final reduction·inside thmThe Unique Games Theorem

Statement (paper)

The construction of the instances GφG_\varphi is a deterministic polynomial-time explicit construction: for fixed ε,δ\varepsilon,\delta, the number hh of listed matrix-test occurrences is a fixed constant times NEkN_{\mathcal E}^k, each weight is a rational of polynomial binary length, the distinct vertices can be identified and numbered in polynomial time, and the final product graph has (4Q)t(4Q)^t edges and polynomially many vertices with Q=⌈h/τ⌉=O(h)Q=\lceil h/\tau\rceil=O(h), with constraints given by full permutation tables of constant size on the alphabet F2ℓt\F_2^{\ell t} and endpoint indices of O(tlog⁡(h+1))O(t\log(h+1)) bits.

In plain English

For fixed ε,δ\varepsilon,\delta, the final Unique Games instances GφG_\varphi are built by a deterministic polynomial-time procedure: the number of listed matrix-test occurrences is h=O(NEk)h=O(N_{\mathcal E}^k), weights are rationals of polynomial bit length, and the final product graph has (4Q)t(4Q)^t edges, with Q=⌈h/τ⌉=O(h)Q=\lceil h/\tau\rceil=O(h), and polynomially many vertices. Constraints are stored as constant-size full permutation tables on F2ℓt\F_2^{\ell t}, with endpoint indices of O(tlog⁡(h+1))O(t\log(h+1)) bits.

Why it's here

This claim covers the running-time and explicitness part of the theorem. It checks that each stage is polynomial for fixed ε,δ\varepsilon,\delta: listing the occurrences, writing the weights, numbering the vertices, and applying the subdivision lemma and then the tensor power, whose size (4Q)t(4Q)^t is polynomial because tt and τ\tau are constants. Together with the value analysis, this gives a deterministic polynomial-time reduction with explicit instances.
Classified routine:
Standard running-time and size bookkeeping for the reduction. It follows from the subdivision lemma (lem-unweighted-subdivision) and the fact that a t-fold tensor power with constant t and \tau stays polynomial in size.

Uses

lemSubdivision yields unweighted simple game

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Polynomial-time explicit encoding" rests on lem:unweighted-subdivision