claimroutineinferred_dep

Tagged right copies preserve value

Tagging right copies preserves YES and NO values
prepares the distinct-tag 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)

On a NO input, val⁡(Φtag)≤val⁡(Φocc)<βγ\val(\Phi_{\mathrm{tag}})\le\val(\Phi_{\mathrm{occ}})<\beta\gamma. Moreover, the tag-independent lift of the YES labeling of Φocc\Phi_{\mathrm{occ}} to Φtag\Phi_{\mathrm{tag}} preserves every local satisfied fraction.

In plain English

On NO inputs, the tagged game Φtag\Phi_{\mathrm{tag}} has value at most that of Φocc\Phi_{\mathrm{occ}}, hence below βγ\beta\gamma. On YES inputs, lifting the Φocc\Phi_{\mathrm{occ}} labeling independently of the tags preserves every local satisfied fraction.

Why it's here

This step adds tags to right vertices, which is needed for the later distinct-tag simple-graph step, without damaging completeness or soundness from the occurrence multigraph. Soundness holds because any labeling of the tagged right copies yields one for Φocc\Phi_{\mathrm{occ}} with no smaller value, so the NO bound <βγ<\beta\gamma carries over. Completeness holds because a labeling that ignores the tag satisfies exactly the same local fractions as before, so the YES guarantee from the rounding step is kept.
Classified routine:
Standard bookkeeping for a vertex-splitting reduction: an averaging argument turns any labeling of the tagged copies into a labeling of Φocc\Phi_{\mathrm{occ}} with no smaller value, and the tag-independent lift of the YES labeling preserves local fractions. It follows directly from the preceding rounding claim.

Uses

claimRounding weights into unweighted multigraph

Used by

claimFull sequence graph value below 3ν/4claimDistinct-tag graph strongly satisfied on YES

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Tagged right copies preserve value" rests on claim-lem-simple-strong-left-3