claimroutineinferred_dep

Fixed-instance verifier gap from strong-left UG

Raghavendra's theorem on UG gives verifier gap >B−η/2>B-\eta/2 vs ≤A+η/2\le A+\eta/2
turns UG hardness into a gap for JJ
Claim·§8.1 Constraint satisfaction and Vertex Cover·inside corGap hardness from a fixed SDP integrality gap

Statement (paper)

Applying Raghavendra's fixed-instance theorem [RaghavendraThesis09, Theorem 7.9] with tolerance η/2\eta/2, whose premise is supplied by the formulation above and Theorem  with a fixed alphabet [M][M] determined by JJ and η\eta, yields verifier instances whose optimum is greater than B−η/2B-\eta/2 in the YES case and at most A+η/2A+\eta/2 in the NO case.

In plain English

Applying Raghavendra's fixed-instance theorem with tolerance η/2\eta/2 to hard Unique Games instances over a fixed alphabet [M][M] (depending on JJ and η\eta) gives verifier instances with optimum greater than B−η/2B-\eta/2 when the formula is satisfiable and at most A+η/2A+\eta/2 when it is not.

Why it's here

This is the step where the hardness of Unique Games is turned into a gap for the fixed instance JJ. Its premise is the padded, uniform-arity form of Λ\Lambda from the previous claim, and the Unique Games input comes from the theorem and the strong-left lemma. Later claims then round the verifier's local law to rationals, so the final instances stay within the stated η\eta slack.
Classified routine:
A direct application of Raghavendra's fixed-instance theorem (Raghavendra's thesis 2009, Theorem 7.9) with tolerance η/2. Its Unique Games premise is supplied by the paper's UG theorem and the strong-left lemma, which is standard bookkeeping.

Uses

thmThe Unique Games TheoremlemUnique Games with constant left degree and strong satisfactionclaimPadding predicates to common arity

Used by

claimRational approximation of local lawclaimRationalization changes optimum by under eta/2

Sources

PaperOpen
Section
§8.1 Constraint satisfaction and Vertex Cover
Page
—
Label
—
Line
sections/07-consequences.tex:89
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Fixed-instance verifier gap from strong-left UG" rests on lem:simple-strong-left
  • info
    inferred_dep
    outline: "Fixed-instance verifier gap from strong-left UG" rests on claim-cor-raghavendra-consequence-1