claimroutine

Effective choice of latent and shortcode parameters

Chooses p∗p_*, τ\tau, r∗r_*, η\eta, α\alpha, rsr_{\rm s} and ℓ\ell effectively
first batch of fixed parameters
Claim·§7.2 The final reduction·inside thmThe Unique Games Theorem

Statement (paper)

Given the rational budgets, one can effectively choose positive rational parameters p∗≤ε0/tp_*\le\eps_0/t and τ≤min⁡{1/200,ε0/t}\tau\le\min\{1/200,\eps_0/t\}, the latent rank threshold r∗r_* from Lemma , η=2−r∗/16\eta=2^{-r_*}/16, shortcode parameters α,rs\alpha,r_{\rm s} (with α\alpha a positive rational lower bound), and a sufficiently large ℓ\ell as in Equation , together with latent data (V,K,C,μ)(\mathcal V,K,C,\mu) with computable rational noise law and a splitting V=K⊕W\mathcal V=K\oplus W, K=F2ℓK=\F_2^\ell, by terminating deterministic constructions; here the thresholds, including m0(η,ℓ)m_0(\eta,\ell) once ℓ\ell is fixed, are supplied by the effective assertions of Lemma  and the effective bounds after Theorem .

In plain English

Given the rational error budgets, all parameters of the final reduction can be chosen effectively: p∗≤ε0/tp_*\le\eps_0/t, τ≤min⁡{1/200,ε0/t}\tau\le\min\{1/200,\eps_0/t\}, the threshold r∗r_*, η=2−r∗/16\eta=2^{-r_*}/16, shortcode parameters α\alpha (a positive rational lower bound) and rsr_{\rm s}, and a large enough ℓ\ell. The latent data (V,K,C,μ)(\mathcal V,K,C,\mu) with computable rational noise law and a splitting V=K⊕W\mathcal V=K\oplus W, K=F2ℓK=\F_2^\ell, can also be built by terminating deterministic procedures.

Why it's here

This claim makes the parameter choices in the final reduction computable, so the reduction is deterministic and polynomial-time with constants depending only on ε,δ\varepsilon,\delta. It does this by feeding the budget p∗p_* into the latent gadget lemma to get r∗r_* and the noise data. It then sets η\eta from r∗r_* and takes the shortcode theorem's α\alpha and rsr_{\rm s} from that η\eta, and fixes ℓ\ell large enough for both. The next step, choosing the cube and parity error, builds on these fixed parameters.
Classified routine:
Parameter bookkeeping: it chains the effective thresholds supplied by the latent gadget lemma (lem-latent) and the effective bounds after the inverse shortcode theorem (thm-shortcode) to make each choice computable. No new idea is involved.

Uses

lemLatent alphabet gadget with detecting noisethmInverse shortcode theorem

Used by

claimChoosing the cube k and parity error

Sources

PaperOpen
Section
§7.2 The final reduction
Page
—
Label
—
Line
sections/06-finish.tex:114
Leannot aligned

Phase 2 aligns this node to a Lean declaration.