claimroutineinferred_dep

Construction runs in polynomial time

Reduction runs in deterministic polynomial time, O(Nh+1)O(N^{h+1}) left vertices
efficiency part of the lemma
Claim·§A.1 A simple strong-left form of Unique Games·inside lemUnique Games with constant left degree and strong satisfaction

Statement (paper)

If NN bounds the explicit size of Φ0\Phi_0, then ∣X1∣=O(N)|X_1|=O(N) and α=L2∣Y∣=O(N)\alpha=L_2|Y|=O(N). The retained graph has ∣X1∣αh(T)h=O(Nh+1)|X_1|\alpha^h(T)_h=O(N^{h+1}) left vertices and hh edges per left vertex, and its identifiers, the rational arithmetic used for rounding, and its permutation tables have polynomial bit length over the fixed alphabet inherited from Φ0\Phi_0; hence the construction φ↦Φφ\varphi\mapsto\Phi_\varphi is computable in deterministic polynomial time.

In plain English

If NN bounds the explicit size of Φ0\Phi_0, then ∣X1∣=O(N)|X_1|=O(N) and α=L2∣Y∣=O(N)\alpha=L_2|Y|=O(N), and the retained graph has O(Nh+1)O(N^{h+1}) left vertices with hh edges each. Its identifiers, rounding arithmetic and permutation tables have polynomial bit length, so φ↦Φφ\varphi\mapsto\Phi_\varphi is computable in deterministic polynomial time.

Why it's here

This is the efficiency part of the reduction in the lemma: since hh, ζ\zeta, ν\nu, dd and HH are fixed constants, the Nh+1N^{h+1} vertex count is polynomial in the input. Together with the completeness step (the distinct-tag graph is strongly satisfied on YES instances), it shows the construction is a legitimate polynomial-time reduction from 3SAT.
Classified routine:
Standard polynomial-time size and bit-length bookkeeping for a reduction with fixed constants h, ζ, ν, d, H, applied to the construction of the earlier claims.

Uses

claimDistinct-tag graph strongly satisfied on YES

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Construction is polynomial size" rests on claim-lem-simple-strong-left-6