7 The main theorem

The statement below is the formalization target of the whole project. It matches, definition for definition, the Lean file MIPRE/HaltingGameValue.lean, which states it on top of Mathlib alone (theorem halting_reduces_to_gameValue): Turing machines are Mathlib’s Nat.Partrec.Code, games are game descriptions (Definition 2.24), and the value is the synchronous value (Definition 2.10).

Theorem 7.1 Halting reduces to the game value; Theorem 12.2 of [ 1 ] , synchronous form

There is a computable map \(g\) from Turing machines to game descriptions such that for every Turing machine \(\cal {M}\):

(Completeness) if \(\cal {M}\) halts on the empty input, then \(\mathrm{val}^{s}(\mathfrak {G}_{g(\cal {M})}) = 1\);
(Soundness) if \(\cal {M}\) does not halt on the empty input, then \(\mathrm{val}^{s}(\mathfrak {G}_{g(\cal {M})}) \leq \tfrac 12\).

Theorem 7.1 follows from Theorem 6.9 by converting the normal form verifier at a fixed index into an explicit game description (a finite object obtained by running the sampler and decider), and relaxing polynomial-time computability of the reduction to computability, per Section 1.3.

Corollary 7.2 Uncomputability of the game value

There is no algorithm that, given a game description \(g\) with the promise that \(\mathrm{val}^{s}(\mathfrak {G}_g) = 1\) or \(\mathrm{val}^{s}(\mathfrak {G}_g) \leq \frac12\), decides which is the case.

Theorem 7.3 \(\mathrm{MIP}^*= \mathrm{RE}\)

\(\mathrm{MIP}^*= \mathrm{RE}\).

For \(\mathrm{RE}\subseteq \mathrm{MIP}^*\): the halting problem is \(\mathrm{RE}\)-complete (Theorem 3.9) and Theorem 6.9 provides a polynomial-time verifier for it; the bridge results (Lemma 2.13 and Theorem 3.3) transfer the completeness–soundness gap from \(\mathrm{val}^{s}\) to \(\mathrm{val}^*\) as required by Definition 2.29. For \(\mathrm{MIP}^*\subseteq \mathrm{RE}\): given a verifier for \(L\) and an input \(z\), enumerate tensor-product strategies (Lemma 3.13) and accept upon finding one with value greater than \(\frac12\); this semi-decides \(L\).

Remark 7.4

The polynomial-time version of Theorem 7.1 (Theorem 12.2 of [ 1 ] as stated there) is recorded by Theorem 6.9; the computable version above is what the Lean main statement asserts, and is sufficient for every consequence in Section 8.