claimroutineinferred_dep

Choosing the cube k and parity error

Chooses a large cube kk, then a small parity error ξ\xi
fixes remaining parameters for the YES/NO analysis
Claim·§7.2 The final reduction·inside thmThe Unique Games Theorem

Statement (paper)

There is a cube k≥8k\ge8, computable by enumeration depending only on the two prescribed errors, such that with m=1+2km=1+2k and β=k−2/3\beta=k^{-2/3} the following hold: kk is large enough for Proposition ; m≥m0(η,ℓ)m\ge m_0(\eta,\ell); α2322(ℓ−rs)(m−rs)>(2rs+1)(ℓ+m)\frac{\alpha^2}{32}2^{(\ell-r_{\rm s})(m-r_{\rm s})}>(2r_{\rm s}+1)(\ell+m); 14[(1+∣V∣−13β2)k−1]<γ12(1+α/4)2\frac14\left[\left(1+\frac{|\mathcal V|-1}{3}\beta^2\right)^k-1\right]<\frac{\gamma_1^2}{(1+\alpha/4)^2}; and (1−β 2−dim⁡W−rs3600)k<γ\left(1-\frac{\beta\,2^{-\dim W-r_{\rm s}}}{3600}\right)^k<\gamma. Moreover, with kk fixed, there is a positive rational ξ<min⁡{1/100,ε0/(2kt)}\xi<\min\{1/100,\eps_0/(2kt)\}, and all these choices depend only on the two prescribed errors, with r∗r_* fixed before ℓ\ell, the advice dimensions before kk, and kk before ξ\xi.

In plain English

One can effectively choose a cube k≥8k\ge8 (with m=1+2km=1+2k, β=k−2/3\beta=k^{-2/3}) satisfying all the largeness conditions the final reduction needs, and then a small positive rational parity error ξ<min⁡{1/100,ε0/(2kt)}\xi<\min\{1/100,\eps_0/(2kt)\}. Every choice depends only on the two prescribed errors.

Why it's here

The conditions on kk are the thresholds from the matrix-gap proposition, the good-row-advice and projected-witness lemmas, the projected-TV lemma (via m≥m0m\ge m_0), and the matrix-decoding and clean-coordinates decay bounds, all of which need kk large. Each holds for all sufficiently large cubes once the earlier parameters are fixed, so one enumerates to find such a kk and then picks ξ\xi small enough that kξk\xi stays within the error budget. The fixed order (r∗r_*, then ℓ\ell, then the advice dimensions, then kk, then ξ\xi) avoids circularity, and the resulting kk and ξ\xi are what the final game's YES/NO value analysis uses.
Classified routine:
Parameter bookkeeping: each condition holds for all sufficiently large cubes once earlier parameters are fixed (by prop-matrix-gap, lem-good-row-advice, lem-projected-witness, lem-projected-tv, lem-clean, prop-matrix-decoding and claim-thm-ugc-2), so enumeration finds k and then a small rational ξ.

Uses

propMatrix game completeness and soundness gaplemGood row advice is common and gives short answer setslemGood advice transfers to projected slicepropMatrix test passing yields decoding strategieslemProjected matrix-test pair is nearly uniformlemAdvice agreement decays with clean coordinatesclaimEffective choice of latent and shortcode parameters

Used by

claimYES and NO values of the final game

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Choosing the cube k and parity error" rests on lem:projected-tv
  • info
    inferred_dep
    outline: "Choosing the cube k and parity error" rests on lem:clean
  • info
    inferred_dep
    outline: "Choosing the cube k and parity error" rests on claim-thm-ugc-2