MIP* = RE

The main theorem, proved: HaltingGameValue.halting_reduces_to_gameValue is the Mathlib-only statement HaltingGameValue.HaltingReducesToGameValue of MIPRE/HaltingGameValue.lean (Theorem 12.2 of "MIP* = RE", blueprint thm:main).

It is the pipeline of MIPRE/Background/Pipeline.lean with its last hypothesis supplied: gap compression is built from introspection (Introspection.seven), answer reduction (AnswerReduction.answerReduction, over the classical PCP decider) and parallel repetition (repetition 7), and a universal machine (Cost.selfUniversal). The consequences of chapter 7 follow unconditionally: the reduction to the quantum value, the uncomputability of both values, and MIP* = RE.

noncomputable def MIPRE.gapCompression : GapCompression

Gap-preserving compression (blueprint thm:compression-target), inhabited.

Equations

• MIPRE.gapCompression = MIPRE.GapCompression.ofAnswerReduction MIPRE.AnswerReduction.answerReduction

theorem HaltingGameValue.halting_reduces_to_gameValue : HaltingReducesToGameValue

Theorem 12.2 of "MIP = RE"* (blueprint thm:main): halting reduces to the synchronous game value.

theorem MIPRE.Halting.halting_reduction_quantum : ∃ (g : Nat.Partrec.Code → HaltingGameValue.GameData), Computable g ∧ ∀ (pc : Nat.Partrec.Code), (HaltingGameValue.HaltsOnEmptyInput pc → quantumValue (g pc).game = 1) ∧ (¬HaltingGameValue.HaltsOnEmptyInput pc → quantumValue (g pc).game ≤ 1 / 2)

Halting reduces to the quantum value (blueprint cor:main-quantum).

theorem MIPRE.Halting.gameValue_uncomputable : ¬∃ (f : HaltingGameValue.GameData → Bool), Computable f ∧ (∀ (d : HaltingGameValue.GameData), HaltingGameValue.gameValue d.toGame = 1 → f d = true) ∧ ∀ (d : HaltingGameValue.GameData), HaltingGameValue.gameValue d.toGame ≤ 1 / 2 → f d = false

The synchronous value is uncomputable (blueprint cor:value-uncomputable).

theorem MIPRE.Halting.quantumValue_uncomputable : ¬∃ (f : HaltingGameValue.GameData → Bool), Computable f ∧ (∀ (d : HaltingGameValue.GameData), quantumValue d.game = 1 → f d = true) ∧ ∀ (d : HaltingGameValue.GameData), quantumValue d.game ≤ 1 / 2 → f d = false

The quantum value is uncomputable (blueprint cor:value-uncomputable, second clause).

theorem MIPRE.Halting.re_subset_mipstarComputable {L : Set Cost.BitStr} (h : IsRE L) : MIPStarComputable L

RE ⊆ MIP*.

theorem MIPRE.Halting.mipstarComputable_eq_re : MIPStarComputable = IsRE

MIP* = RE (blueprint thm:mipstar-eq-re).

theorem MIPRE.Halting.re_subset_mipstar {L : Set Cost.BitStr} (h : IsRE L) : MIPStar L

RE ⊆ MIP*_{1,1/2}(2,1), the paper's class: a polynomial-time sampler and decider.

theorem MIPRE.Halting.mipstar_eq_re : MIPStar = IsRE

MIP*_{1,1/2}(2,1) = RE (blueprint thm:mipstar-eq-re), for the paper's class.