claimroutineinferred_dep

Distinct-tag graph strongly satisfied on YES

Distinct-tag graph is simple and strongly satisfies >1−ζ>1-\zeta of left vertices on YES
completeness for the simple graph
Claim·§A.1 A simple strong-left form of Unique Games·inside lemUnique Games with constant left degree and strong satisfaction

Statement (paper)

Let the retained graph be the subgraph on sequence vertices whose tags t1,…,tht_1,\ldots,t_h are pairwise distinct. This graph is simple and every left vertex has degree hh, and it contains a pgraphp_{\mathrm{graph}} fraction of the full set of sequence vertices at each xx. If Φocc\Phi_{\mathrm{occ}} has a labeling satisfying a fraction at least 1−u1-u of the vertices xx, each with satisfied fraction at least 1−a1-a, then the lifted labeling strongly satisfies at least a (1−u)(1−a)h≥1−u−ha=1−(h+1)u−h/L2>1−ζ(1-u)(1-a)^h\ge 1-u-ha=1-(h+1)u-h/L_2>1-\zeta fraction of the left vertices of the retained graph.

In plain English

The retained subgraph on sequence vertices with pairwise distinct tags is simple, has left degree hh, and keeps a pgraphp_{\mathrm{graph}} fraction of the sequence vertices at each xx. If Φocc\Phi_{\mathrm{occ}} has a labeling that satisfies a 1−a1-a fraction at a 1−u1-u fraction of the vertices xx, the lifted labeling strongly satisfies more than a 1−ζ1-\zeta fraction of the retained graph's left vertices.

Why it's here

This is the completeness step for the simple graph. A left vertex is strongly satisfied when all hh of its sampled occurrences are satisfied, which happens with probability at least (1−a)h≥1−ha(1-a)^h\ge 1-ha at each good xx. Combined with the bad xx fraction uu and with a=u+1/L2a=u+1/L_2 from the rounding step, the loss is at most (h+1)u+h/L2<ζ(h+1)u+h/L_2<\zeta. The tagged labeling from the previous step is lifted independently of the tags, so restricting to distinct tags does not change these local fractions.
Classified routine:
Completeness bookkeeping inside the left-degree/strong-satisfaction reduction for Unique Games: it applies the Bernoulli/union bound (1-a)^h ≥ 1-ha to the sampled occurrences and restricts to distinct tags, in the style of standard degree-reduction arguments, using the earlier rounding and tagging claims.

Uses

claimRounding weights into unweighted multigraphclaimTagged right copies preserve value

Used by

claimNO soundness of the retained graphclaimConstruction runs in polynomial time

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Distinct-tag graph simple, YES strongly satisfied" rests on claim-lem-simple-strong-left-3
  • info
    inferred_dep
    outline: "Distinct-tag graph simple, YES strongly satisfied" rests on claim-lem-simple-strong-left-4