Documentation

MIPRE.TailoredMIP

TMIP* = RE, and the Aldous–Lyons conjecture is false #

The main theorem of The Aldous–Lyons Conjecture II: Undecidability (Bowen–Chapman–Vidick, arXiv:2501.00173, thm:tailored_MIP*=RE, II:1505), proved: TailoredGameValue.tailored_halting_reduction is the Mathlib-only statement TailoredGameValue.TailoredHaltingReduction of MIPRE/TailoredGameValue.lean (blueprint thm:tmip-re). Tailored compression is built from question reduction (Intro.Inhabit.tailoredIntrospection), answer reduction (AnsRed.Typed.tailoredAnswerReduction) and parallel repetition (tailoredRepetition), and the class theorems follow for both readings of TMIP*.

With paper I (The Aldous–Lyons Conjecture I: Subgroup Tests, Bowen–Chapman–Lubotzky–Vidick, arXiv:2408.00110), the sofic value of subgroup tests is not approximable and the Aldous–Lyons conjecture is false: SubgroupTestValue.aldous_lyons_false is the negation of the Mathlib-only statement SubgroupTestValue.AldousLyons of MIPRE/SubgroupTestValue.lean (blueprint thm:aldous-lyons-false).

source
noncomputable def MIPRE.Tailored.tailoredGapCompression :
TailoredGapCompression 7

Tailored gap compression (blueprint thm:tailored-compression-target), inhabited.

Equations
Instances For
    source
    theorem TailoredGameValue.tailored_halting_reduction :
    TailoredHaltingReduction

    TMIP* = RE (paper II, thm:tailored_MIP*=RE, II:1505; blueprint thm:tmip-re): the halting problem reduces to tailored games, with a perfect ZPC strategy on the machines that halt and synchronous value at most 1/2 on the others.

    source
    theorem MIPRE.Tailored.tailored_halting_reduction_quantum :
    ∃ (g : Nat.Partrec.Code → TailoredGameValue.TailoredGameData), Computable g ∧ ∀ (c : Nat.Partrec.Code), (HaltingGameValue.HaltsOnEmptyInput c → (g c).HasPerfectZPC) ∧ (¬HaltingGameValue.HaltsOnEmptyInput c → quantumValue (g c).game ≤ 1 / 2)

    The halting problem reduces to tailored games, in the quantum value.

    source
    theorem MIPRE.Tailored.tmipStarComputable_eq_re :
    TMIPStarComputable = IsRE

    TMIP* = RE, computable class (II:787, II:6997).

    source
    theorem MIPRE.Tailored.tmipStar_eq_re :
    TMIPStar = IsRE

    TMIP* = RE, the paper's polynomial-time class (II:787).

    source
    theorem SubgroupTestValue.not_sofValueApproximable :
    ¬SofValueApproximable

    The sofic value of subgroup tests is not approximable (paper I, Corollary I:2144, measure-free).

    source
    theorem SubgroupTestValue.aldous_lyons_false :
    ¬AldousLyons

    The Aldous–Lyons conjecture is false (paper I, Corollary I:2144, with paper II's main theorem; blueprint thm:aldous-lyons-false).