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.43), and the value is the synchronous value (Definition 2.10).
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\).
MIPRE.Halting.halting_reduces_to_gameValue_of takes a MIPRE.GapCompression and a universal machine and concludes exactly this statement; Theorem 6.198 supplies the compression.
Status. The theorem is proved in Lean, with no hypothesis: HaltingGameValue.halting_reduces_to_gameValue (MIPRE/MainTheorem.lean) proves the proposition HaltingGameValue.HaltingReducesToGameValue, which MIPRE/HaltingGameValue.lean states on top of Mathlib alone. The proof cannot live in that file, which imports nothing else; it is the conditional MIPRE.Halting.halting_reduces_to_gameValue_of at the compression of Theorem 6.198, built from the supplied introspection, answer-reduction and repetition stages (Corollary 6.199), and it depends on the axioms propext, Classical.choice and Quot.sound only.
Theorem 7.1 reads the computable explicit-game conclusion of Theorem 6.214 in the synchronous value. Its construction tabulates a normal form verifier at a fixed index. The source’s polynomial-time reduction constructs sampler and decider programs; passing to the explicit finite table establishes computability, with no polynomial bound on enumeration asserted (Section 1.3). A game description rejects unequal answers to equal questions by fiat (Definition 2.43), which costs nothing here: against a tracial state a projective family is perfectly consistent, so the terms the fiat deletes carry no weight in \(\mathrm{val}^{s}\), which is unchanged, and it can only lower \(\mathrm{val}^*\) — the safe direction for the soundness clause, while the completeness witness is synchronous and survives. The two passages this needs from Theorem 6.214, whose Lean assembly concludes in \(\mathrm{val}^*\), are formalized: the transport of a value-\(1\) PCC strategy along the relabelings of the tabulation (MIPRE.Verifier.gameValue_toGame_eq_one_doubled, through MIPRE.syncValue_eq_of_equiv) for completeness, and MIPRE.Verifier.gameValue_toGame_le_of_valStar_le_doubled for soundness; both are stated directly in HaltingGameValue.gameValue, by Remark 7.2’s identification of the two vocabularies, and both are read against the doubled game of \(\mathsf{V}_n\), which is how the tabulation matches it without asking the verifier to be synchronous (Remark 6.204, item 3). On the tabulation the completeness bridge is MIPRE.Halting.gameValue_tab_eq_one. The four obligations of Theorem 6.214 are all discharged (MIPRE.Halting.exists_obligations), so nothing but Theorem 6.198 stands between the conditional and the unconditional statement. The record of the tabulation’s agreement with \(\mathsf{V}_n\) in the form the completeness bridge consumes is MIPRE.Halting.tab_match (Remark 6.204), and MIPRE.Halting.halting_reduction_both_of is the one map carrying both readings of the value at once, which is what Corollary 7.3 asks.
The Lean main statement is deliberately self-contained: the file MIPRE/HaltingGameValue.lean imports nothing from the rest of this development, re-declaring the synchronous game, the synchronous strategy and the value on top of Mathlib alone, so that Theorem 7.1 can be read without any of the vocabulary built in Section 2. In that reduced vocabulary gameValue is the synchronous value of Definition 2.10 and equivTuple exhibits the canonical Gödel numbering asserted in Definition 2.43 as an explicit equivalence between game descriptions and a tuple of integers and lists, which is what supplies the Encodable instance the computability clause quantifies over. The duplication is the price of a statement that stands alone, and keeping the two vocabularies in step is a maintenance obligation rather than a mathematical one: the definitions match one for one, and this is the list of the ones that do. The correspondence is not left to inspection where it is used: GameData.syncGame and GameData.game read a description in the vocabulary of Section 2 with the same distribution and predicate, and GameData.gameValue_eq_syncValue proves the two synchronous values equal — the two structures of synchronous strategy, one carrying POVMs with a projectivity certificate and the other a ProjectiveMeasurement, repackage into each other with the same dimension and the same operators, so the two suprema are over the same set of numbers. GameData.gameValue_le_quantumValue is the comparison \(\mathrm{val}^{s}\leq \mathrm{val}^*\) (Lemma 2.14) in that vocabulary.
With \(g\) as in Theorem 7.1: if \(\cal {M}\) halts on the empty input then \(\mathrm{val}^*(\mathfrak {G}_{g(\cal {M})}) = 1\), and if \(\cal {M}\) does not halt on the empty input then \(\mathrm{val}^*(\mathfrak {G}_{g(\cal {M})}) \leq \tfrac 12\).
At the compression of Theorem 6.198, as Theorem 7.1 is: MIPRE.Halting.halting_reduction_both_of produces one computable map with both values, the quantum one from tab_value and Verifier.valStar_eq_one_of_hasPerfectPCC in the halting branch and from tab_value alone in the other; the corollary is its quantum half.
Both forms come from the two items of Theorem 6.214 directly: the value-\(1\) witness is an ambient synchronous PCC strategy, so it gives value \(1\) in both senses; and the soundness conclusion is \(\mathrm{val}^*(\mathfrak {G}_\cal {M}) \leq \frac12\), which gives \(\mathrm{val}^{s}(\mathfrak {G}_\cal {M}) \leq \frac12\) by Lemma 2.14. The quantum form is the one Definition 2.53 asks for, and it is the primary one: no transport from \(\mathrm{val}^{s}\) to \(\mathrm{val}^*\) is involved anywhere, the pipeline’s soundness being carried in \(\mathrm{val}^*\) at every step (Remark 6.8). The synchronous reading of Theorem 7.1 is the derived one, obtained from this corollary by the free comparison \(\mathrm{val}^{s}\leq \mathrm{val}^*\).
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; the same holds with \(\mathrm{val}^*\) in place of \(\mathrm{val}^{s}\) (Corollary 7.3).
A computable \(f\) answering true on every description of value \(1\) and false on every description of value at most \(\frac12\), composed with the map of Theorem 7.1 (respectively Corollary 7.3), would decide whether a machine halts on the empty input, against Theorem 3.79. In Lean the algorithm is a Mathlib-computable Boolean function (Halting/Corollaries.lean), at the compression of Theorem 6.198.
Every language in \(\mathrm{MIP}^*\) is recursively enumerable.
Let \(z \mapsto \mathfrak {G}_z\) witness \(L \in \mathrm{MIP}^*\). Under the promise, \(z \in L\) if and only if \(\mathrm{val}^*(\mathfrak {G}_z) {\gt} \frac12\): the value is \(1\) on \(L\) and at most \(\frac12\) off it. By Lemma 3.112 the set of game descriptions \(g\) with \(\mathrm{val}^*(\mathfrak {G}_g) {\gt} \frac12\) is recursively enumerable, and \(L\) is its preimage under the computable map \(z \mapsto \mathfrak {G}_z\); the preimage of an r.e. set under a computable map is r.e. Concretely: given \(z\), compute \(\mathfrak {G}_z\), enumerate tensor-product strategies and accept upon finding one of value greater than \(\frac12\); this semi-decides \(L\). In Lean the class is the computable one (Definition 2.53), and MIPStarComputable.exists_semidecider gives the semidecider as a program of the ambient model.
For \(\mathrm{RE}\subseteq \mathrm{MIP}^*\): the halting problem is \(\mathrm{RE}\)-complete (Theorem 3.79) and Theorem 6.214 provides a computable map to explicit games, whose completeness–soundness gap is already in the form the computable class of Definition 2.53 requires (Corollary 7.3); no transport between the two values is needed. \(\mathrm{MIP}^*\subseteq \mathrm{RE}\) is Lemma 7.5. In Lean the many-one reduction of an r.e. language to halting on the empty input is MIPRE.IsRE.exists_code_halts, from Mathlib’s Nat.Partrec.Code.curry, for the computable class of Definition 2.53 (MIPRE.Halting.mipstarComputable_eq_re); the equality holds at the compression of Theorem 6.198, as Theorem 7.1 does.
For the class of Definition 2.52, MIPRE.Halting.mipstar_eq_re: \(\mathrm{MIP}^*\subseteq \mathrm{RE}\) is Lemma 2.54, and \(\mathrm{RE}\subseteq \mathrm{MIP}^*\) (re_subset_mipstar) is the polynomial-time form of Theorem 6.214. An r.e. language many-one reduces to halting on the empty input by a polynomial-time map \(z \mapsto \cal {M}_z\) (Cost.exists_polyTime_reduction: the semidecider with \(z\) hardcoded), and the class verifier of Theorem 6.214 on input \(z\) plays the game of \(\mathsf{V}^{\mathsf{halt}}_{\cal {M}_z, \lambda (\cal {M}_z)}\) at the fixed level \(C\), whose value is \(1\) if \(\cal {M}_z\) halts and at most \(\frac12\) if not.
The source polynomial-time reduction constructs efficient sampler and decider descriptions (Theorem 12.2 of [ 1 ] ), as distinguished after Theorem 6.214; it is what the class of Definition 2.52 asks for, and the case of the theorem proved through re_subset_mipstar. The computable explicit-table version is the case for the class of Definition 2.53, and is sufficient for every consequence in Section 8.