claimroutineinferred_dep

Explicit polynomial-size occurrence list

Rationalized instance is an explicit polynomial-size occurrence list
shows the output is computable in polynomial time
Claim·§8.1 Constraint satisfaction and Vertex Cover·inside corGap hardness from a fixed SDP integrality gap

Statement (paper)

The occurrence list on the variable set VΦ×DMV_\Phi\times D^M, with one occurrence for each s∈Ss\in\mathcal S, u∈LΦu\in L_\Phi and ordered neighbor tuple in N(u)a(s)N(u)^{a(s)}, where the occurrence applies the Λ\Lambda-predicate prescribed by ss to the resulting query variables and has weight θ^(s)/(∣LΦ∣ha(s))\widehat\theta(s)/(|L_\Phi|h^{a(s)}), has nonnegative rational weights summing to one. It consists of ∣LΦ∣∑s∈Sha(s)|L_\Phi|\sum_{s\in\mathcal S}h^{a(s)} occurrences on ∣VΦ∣∣D∣M|V_\Phi||D|^M variables, and it can be written down in time polynomial in the size of the input, with each weight of polynomial binary length.

In plain English

The rationalized instance is given by an explicit list of occurrences on the variables VΦ×DMV_\Phi\times D^M, one for each s∈Ss\in\mathcal S, vertex u∈LΦu\in L_\Phi and ordered tuple of neighbors in N(u)a(s)N(u)^{a(s)}. Its weights θ^(s)/(∣LΦ∣ha(s))\widehat\theta(s)/(|L_\Phi|h^{a(s)}) are nonnegative rationals summing to one, it has ∣LΦ∣∑sha(s)|L_\Phi|\sum_{s}h^{a(s)} occurrences, and it can be written down in polynomial time with polynomially long weights.

Why it's here

This shows the reduction's output is a genuine, efficiently computable Λ\Lambda-instance. It uses the rational table θ^\widehat\theta from the previous claim, which makes the weights rational with constant-size description, and the constant left degree hh from the Unique Games lemma, which keeps the number of neighbor tuples polynomial. The later claims can then compare this instance's value to the original verifier's value, and the reduction is polynomial-time.
Classified routine:
Straightforward bookkeeping: summing the weights over the |L_Φ|h^{a(s)} neighbor tuples per s recovers the rational law θ̂, and polynomial size follows from the constant left degree h (lem-simple-strong-left) and the constant-size rational table θ̂ (previous claim).

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Explicit polynomial occurrence list" rests on lem:simple-strong-left
  • info
    inferred_dep
    outline: "Explicit polynomial occurrence list" rests on claim-cor-raghavendra-consequence-3