claimroutineinferred_dep

NO soundness of the retained graph

Retained graph has value below ν\nu on NO inputs
soundness case 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 φ\varphi is unsatisfiable, then val⁡(Φφ)<ν\val(\Phi_\varphi)<\nu: any labeling of the retained graph extends, by assigning arbitrary labels to discarded left vertices and keeping all right labels, to a labeling of the full graph whose full edge value is at least pgraphp_{\mathrm{graph}} times its retained edge value, and by the retained edge value is at most s/pgraph<(3ν/4)/(3/4)=νs/p_{\mathrm{graph}}<(3\nu/4)/(3/4)=\nu.

In plain English

If φ\varphi is unsatisfiable, then the retained simple Unique Games graph Φφ\Phi_\varphi has value less than ν\nu.

Why it's here

Any labeling of the retained graph extends to the full sequence graph by labeling discarded left vertices arbitrarily and keeping right labels, and the full value is at least pgraphp_{\mathrm{graph}} times the retained edge value. Combined with the full-graph bound s<3ν/4s<3\nu/4 and pgraph≥3/4p_{\mathrm{graph}}\ge 3/4, the retained value is below (3ν/4)/(3/4)=ν(3\nu/4)/(3/4)=\nu, giving the NO case of the parent lemma.
Classified routine:
Direct consequence of the full-graph soundness bound (claim 5) and the retained-fraction bound p_graph ≥ 3/4 (claim 6), using the standard argument of extending a labeling from the retained subgraph to the full graph.

Uses

claimFull sequence graph value below 3ν/4claimDistinct-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:210
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "NO soundness of retained graph" rests on claim-lem-simple-strong-left-5
  • info
    inferred_dep
    outline: "NO soundness of retained graph" rests on claim-lem-simple-strong-left-6