Table of Contents
Fetching ...

The Aldous--Lyons Conjecture II: Undecidability

Lewis Bowen, Michael Chapman, Thomas Vidick

TL;DR

This work proves an undecidability result for the Aldous–Lyons conjecture by constructing tailored non-local games whose ZPC (Z-aligned permutation) perfect strategies can be distinguished from all strategies that are far from perfect only via an RE-hard Halting-problem-like reduction. The authors develop a compression framework that converts long-question games into poly-length instances while preserving completeness and soundness, through three transformations: introspection (QuestionReduction), PCP-based AnswerReduction, and ParallelRepetition. Central technical innovations include adapting compression to the tailored game setting, leveraging the Pauli group to enforce sampling and measurement universality, and building a robust Pauli-basis self-test to anchor question distributions and linear constraints. The resulting TailoredMIP* = RE theorem yields a negative resolution to Aldous–Lyons, with implications for unimodular networks and Connes’ embedding problem, and connects hardness of quantum verification to deep operator-algebraic questions. The approach advances the MIP* paradigm by introducing a middle-ground class of tailored games that balance linear and nonlinear verification to retain group-theoretic structure while enabling undecidability results with controlled strategy restrictions.

Abstract

This paper, and its companion [BCLV24], are devoted to a negative resolution of the Aldous--Lyons Conjecture [AL07, Ald07]. In this part we study tailored non-local games. This is a subclass of non-local games -- combinatorial objects which model certain experiments in quantum mechanics, as well as interactive proofs in complexity theory. Our main result is that, given a tailored non-local game $G$, it is undecidable to distinguish between the case where $G$ has a special kind of perfect strategy, and the case where every strategy for $G$ is far from being perfect. Using a reduction introduced in the companion paper [BCLV24], this undecidability result implies a negative answer to the Aldous--Lyons conjecture. Namely, it implies the existence of unimodular networks that are non-sofic. To prove our result, we use a variant of the compression technique developed in MIP*=RE [JNV+21]. Our main technical contribution is to adapt this technique to the class of tailored non-local games. The main difficulty is in establishing answer reduction, which requires a very careful adaptation of existing techniques in the construction of probabilistically checkable proofs. As a byproduct, we are reproving the negation of Connes' embedding problem [Con76] -- i.e., the existence of a $\mathrm{II}_1$-factor which cannot be embedded in an ultrapower of the hyperfinite $\mathrm{II}_1$-factor -- first proved in [JNV+21], using an arguably more streamlined proof. In particular, we incorporate recent simplifications from the literature [dlS22b, Vid22] due to de la Salle and the third author.

The Aldous--Lyons Conjecture II: Undecidability

TL;DR

This work proves an undecidability result for the Aldous–Lyons conjecture by constructing tailored non-local games whose ZPC (Z-aligned permutation) perfect strategies can be distinguished from all strategies that are far from perfect only via an RE-hard Halting-problem-like reduction. The authors develop a compression framework that converts long-question games into poly-length instances while preserving completeness and soundness, through three transformations: introspection (QuestionReduction), PCP-based AnswerReduction, and ParallelRepetition. Central technical innovations include adapting compression to the tailored game setting, leveraging the Pauli group to enforce sampling and measurement universality, and building a robust Pauli-basis self-test to anchor question distributions and linear constraints. The resulting TailoredMIP* = RE theorem yields a negative resolution to Aldous–Lyons, with implications for unimodular networks and Connes’ embedding problem, and connects hardness of quantum verification to deep operator-algebraic questions. The approach advances the MIP* paradigm by introducing a middle-ground class of tailored games that balance linear and nonlinear verification to retain group-theoretic structure while enabling undecidability results with controlled strategy restrictions.

Abstract

This paper, and its companion [BCLV24], are devoted to a negative resolution of the Aldous--Lyons Conjecture [AL07, Ald07]. In this part we study tailored non-local games. This is a subclass of non-local games -- combinatorial objects which model certain experiments in quantum mechanics, as well as interactive proofs in complexity theory. Our main result is that, given a tailored non-local game , it is undecidable to distinguish between the case where has a special kind of perfect strategy, and the case where every strategy for is far from being perfect. Using a reduction introduced in the companion paper [BCLV24], this undecidability result implies a negative answer to the Aldous--Lyons conjecture. Namely, it implies the existence of unimodular networks that are non-sofic. To prove our result, we use a variant of the compression technique developed in MIP*=RE [JNV+21]. Our main technical contribution is to adapt this technique to the class of tailored non-local games. The main difficulty is in establishing answer reduction, which requires a very careful adaptation of existing techniques in the construction of probabilistically checkable proofs. As a byproduct, we are reproving the negation of Connes' embedding problem [Con76] -- i.e., the existence of a -factor which cannot be embedded in an ultrapower of the hyperfinite -factor -- first proved in [JNV+21], using an arguably more streamlined proof. In particular, we incorporate recent simplifications from the literature [dlS22b, Vid22] due to de la Salle and the third author.
Paper Structure (81 sections, 38 theorems, 534 equations, 17 figures, 4 tables)

This paper contains 81 sections, 38 theorems, 534 equations, 17 figures, 4 tables.

Key Result

Theorem 1.1

There exists a polynomial time algorithm that takes as input a Turing machine $\mathcal{M}$ and outputs a tailored non-local game $\mathfrak{G}_\mathcal{M}$ such that:

Figures (17)

  • Figure 1: In this figure there are $5$ permutations, $-{\rm Id}, \mathds{X}^{\otimes 01},\mathds{X}^{\otimes 10},\mathds{Z}^{\otimes 01},\mathds{Z}^{\otimes 10}$, acting on the set $(\mathbb{F}_2^2)_{\pm}$. The $\mathds{X}$ permutations act as bit flips. The $\mathds{Z}$ permutations are conditional sign changes, namely, they flip the sign depending on whether the associated bit is $0$ or $1$. Finally, $-{\rm Id}$ flips the sign.
  • Figure 2: This is an example of the actions of the Pauli matrices on $Y_\pm$, which consists of all signed bit strings of length $3$ in this case. The purple dashed lines are the actions of $-{\rm Id}$. The shades of green solid lines are the actions of the $\mathds{X}$-generators for the standard basis elements. The shades of blue dotted lines are the actions of the $\mathds{Z}$-generators. We intentionally did not include all actions of $\mathds{Z}$-generators, for visual clarity.
  • Figure 3: Questions and answers in the generalized Pauli basis game ${\mathfrak{Pauli\ Basis}}_k(\mathscr{B})$. Since the game is tailored as an LCS, all answers are unreadable. We also list the conditions on a strategy's observables that the game enforces.
  • Figure 4: The underlying graph of the commutation game $\frak{C}$.
  • Figure 5: The underlying graph of the anti-commutation game $\frak{M}$.
  • ...and 12 more figures

Theorems & Definitions (330)

  • Theorem 1.1: Main Theorem. See Theorem \ref{['thm:tailored_MIP*=RE']} for a formal version. Compare to Theorem 7.4 in BCLV_subgroup_tests
  • Remark 1.2: Asymptotic notation
  • Remark 1.3: Additional conventions throughout the paper
  • Definition 2.1: POVMs and PVMs
  • Definition 2.2: Joint measurements
  • Remark 2.3
  • Definition 2.4: The Fourier transform of a representation
  • Definition 2.5: Projective, Representation and Observable form of a PVM
  • Remark 2.6
  • Definition 2.7: Diagonal PVM
  • ...and 320 more