claimroutineinferred_dep

Explicit rational encoding is polynomial

Output ordering instance is written explicitly in polynomial time
algorithmic part of the proposition
Claim·§A.2 The finite ordering transfer·inside propFinite ordering transfer from Unique Games

Statement (paper)

For fixed RR, the transformation is explicit and deterministic: it outputs the variables V=B×[m]R\mathcal V=B\times[m]^R and, for each a∈Aa\in A, each ordered distinct neighbor tuple and each ξ∈supp⁡θR\xi\in\operatorname{supp}\theta_R, the permuted tuple of with nonnegative rational weight θR(ξ)/(∣A∣(h)k)\theta_R(\xi)/(|A|(h)_k). These weights sum to one, every listed tuple has distinct IDs, there are ∣B∣mR|B|m^R variables and at most ∣A∣(h)k∣supp⁡θR∣|A|(h)_k|\operatorname{supp}\theta_R| entries, each weight has O(log⁡∣A∣+klog⁡h)O(\log|A|+k\log h) bits plus a fixed constant and each ID has O(log⁡∣B∣)O(\log|B|) bits plus a fixed constant, so exact enumeration of the entries takes time polynomial in the explicit size of Φ\Phi for fixed RR.

In plain English

For fixed RR, the transformation deterministically lists variables B×[m]RB\times[m]^R and, for each a∈Aa\in A, ordered distinct neighbor tuple and ξ∈supp⁡θR\xi\in\operatorname{supp}\theta_R, a permuted tuple with distinct IDs and rational weight θR(ξ)/(∣A∣(h)k)\theta_R(\xi)/(|A|(h)_k). The weights sum to one, the encodings are of controlled bit length, and the whole list is produced in time polynomial in the explicit size of Φ\Phi.

Why it's here

This is the algorithmic part of the proposition: it shows the instance whose values were analyzed in the previous claim, with distinct variables in each constraint, can be written out exactly with normalized rational weights. The count is ∣B∣mR|B|m^R variables and at most ∣A∣(h)k∣supp⁡θR∣|A|(h)_k|\operatorname{supp}\theta_R| entries, with RR fixed, so enumeration is polynomial, which gives the deterministic polynomial-time transformation claimed.
Classified routine:
Standard bookkeeping for polynomial-time reductions: it counts the variables and weighted constraint entries and bounds their bit lengths, which follows directly from the construction in the earlier claims with R fixed.

Uses

claimConditioning on distinct neighbors gives strict gap

Used by

Nothing in the paper

Sources

PaperOpen
Section
§A.2 The finite ordering transfer
Page
—
Label
—
Line
appendices/finite-consequences.tex:945
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Explicit rational encoding is polynomial" rests on claim-prop-finite-ordering-transfer-6