lemmaroutine

Preprocessing to distinct variable positions

Makes equation variables distinct; completeness kept, soundness loss small
cleans the parity gap as input to the matrix game
Lemma·lem:distinct-parity·§4.1 Weighted parity equations and distinct positions

Statement (paper)

From a weighted parity instance E\mathcal E one can deterministically construct, in polynomial time, an instance E′\mathcal E' in which the three variable IDs of every occurrence are distinct. Its weights are positive rationals of polynomial bit length, and OPT⁡(E′)≥OPT⁡(E),OPT⁡(E′)≤1+OPT⁡(E)2+3100. \OPT(\mathcal E')\ge\OPT(\mathcal E), \qquad \OPT(\mathcal E') \le \frac{1+\OPT(\mathcal E)}2+\frac3{100}. In particular, Theorem  with ξ<1/100\xi<1/100, followed by this preprocessing, gives completeness at least 1−ξ1-\xi and NO optimum at most 4/54/5.

In plain English

Any weighted parity instance E\mathcal E can be converted deterministically in polynomial time into an instance E′\mathcal E' whose occurrences each have three distinct variable IDs, with positive rational weights of polynomial bit length. The optimum does not decrease, OPT⁡(E′)≥OPT⁡(E)\OPT(\mathcal E')\ge\OPT(\mathcal E), and rises by at most a small amount: OPT⁡(E′)≤1+OPT⁡(E)2+3100\OPT(\mathcal E')\le \frac{1+\OPT(\mathcal E)}2+\frac3{100}.

Why it's here

This lemma removes the degenerate case where an equation repeats a variable, so later steps can assume three distinct positions. It keeps completeness and bounds the soundness loss: applying Theorem thm:parity with ξ<1/100\xi<1/100 and then this step gives completeness at least 1−ξ1-\xi and NO optimum at most 4/54/5, which the Unique Games Theorem reduction uses as its starting gap.
Classified routine:
A standard gadget-style preprocessing of Max-3LIN instances (Håstad-type parity equations) that replaces repeated variables with fresh ones; the soundness accounting rac{1+ ext{OPT}}{2}+ rac{3}{100} is bookkeeping rather than a new idea.

Sources

PaperOpen
Section
§4.1 Weighted parity equations and distinct positions
Page
—
Label
lem:distinct-parity
Line
sections/03-game.tex:48
Leannot aligned

Phase 2 aligns this node to a Lean declaration.