The consequences of the halting reduction, conditionally on compression

Blueprint chapter 7 after thm:main, and thm:halting-undecidable of chapter 3, each proved from a GapCompression (the hypothesis structure of thm:compression) and a universal machine:

• halting_undecidable, halting_re: Turing's theorem, from Mathlib's ComputablePred.halting_problem and halting_problem_re at the empty input.
• gameValue_uncomputable_of, quantumValue_uncomputable_of (cor:value-uncomputable): no computable predicate decides, under the promise that the value is 1 or at most 1/2, which it is — in either value.
• re_subset_mipstarComputable_of and mipstarComputable_eq_re_of (thm:mipstar-eq-re): RE ⊆ MIP* by reducing membership in an r.e. language to halting on the empty input (Nat.Partrec.Code.curry) and composing with the reduction; with MIPStarComputable.isRE, MIP* = RE.

Turing's theorem

theorem MIPRE.halting_undecidable : ¬ComputablePred fun (c : Nat.Partrec.Code) => HaltingGameValue.HaltsOnEmptyInput c

The halting problem is not decidable (blueprint thm:halting-undecidable): Mathlib's ComputablePred.halting_problem at the empty input.

theorem MIPRE.halting_re : REPred fun (c : Nat.Partrec.Code) => HaltingGameValue.HaltsOnEmptyInput c

The halting problem is r.e.

Uncomputability of the value

theorem MIPRE.Halting.not_decidable_of_reduction {P : HaltingGameValue.GameData → Prop} (h : ∃ (g : Nat.Partrec.Code → HaltingGameValue.GameData), Computable g ∧ ∀ (pc : Nat.Partrec.Code), (HaltingGameValue.HaltsOnEmptyInput pc → P (g pc)) ∧ (¬HaltingGameValue.HaltsOnEmptyInput pc → ¬P (g pc))) : ¬∃ (f : HaltingGameValue.GameData → Bool), Computable f ∧ ∀ (d : HaltingGameValue.GameData), P d ↔ f d = true

A computable predicate separating the two sides of a promise problem decides every problem that reduces to it: the shape both halves of cor:value-uncomputable use.

theorem MIPRE.Halting.gameValue_uncomputable_of (G : GapCompression) (U : Cost.UniversalMachine) : ¬∃ (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

Uncomputability of the synchronous value (blueprint cor:value-uncomputable), conditionally on compression: no computable f answers true on every description of synchronous value 1 and false on every description of synchronous value at most 1/2.

theorem MIPRE.Halting.quantumValue_uncomputable_of (G : GapCompression) (U : Cost.UniversalMachine) : ¬∃ (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

Uncomputability of the quantum value (blueprint cor:value-uncomputable, second clause), conditionally on compression.

RE ⊆ MIP*, hence MIP* = RE

theorem MIPRE.Halting.exists_code_halts_of_isRE {L : Set Cost.BitStr} (h : IsRE L) : ∃ (r : Cost.BitStr → Nat.Partrec.Code), Computable r ∧ ∀ (x : Cost.BitStr), HaltingGameValue.HaltsOnEmptyInput (r x) ↔ x ∈ L

Every r.e. language many-one reduces to the halting problem: a computable map from strings to codes, halting on the empty input exactly on the members. Mathlib's Nat.Partrec.Code.curry fixes the string into the code.

theorem MIPRE.Halting.re_subset_mipclass_of_reduction (ω : ValueModel) (hred : ω.HaltingReductionRE) {L : Set Cost.BitStr} (h : IsRE L) : MIPClass ω L

RE ⊆ MIPClass ω, given a halting reduction of RE shape to the value: compose the many-one reduction of an r.e. language to the halting problem with the reduction.

theorem MIPRE.Halting.core_subset_mipclass_of_reduction (ω : ValueModel) (hred : ω.HaltingReductionCoRE) {L : Set Cost.BitStr} (h : IsCoRE L) : MIPClass ω L

coRE ⊆ MIPClass ω, given a halting reduction of coRE shape to the value: the complement of a co-r.e. language reduces to halting on the empty input, and the reduction sends halting machines to value at most 1/2 and the others to value 1.

theorem MIPRE.Halting.mipclass_eq_re_of_reduction (ω : ValueModel) (hlow : ω.LowerRE) (hred : ω.HaltingReductionRE) : MIPClass ω = IsRE

MIPClass ω = RE, given a lower semidecider for the value and a halting reduction of RE shape: the two classes coincide, as predicates on languages.

theorem MIPRE.Halting.mipclass_eq_core_of_reduction (ω : ValueModel) (hup : ω.UpperRE) (hred : ω.HaltingReductionCoRE) : MIPClass ω = IsCoRE

MIPClass ω = coRE, given an upper semidecider for the value and a halting reduction of coRE shape.

theorem MIPRE.Halting.re_subset_mipstarComputable_of (G : GapCompression) (U : Cost.UniversalMachine) {L : Set Cost.BitStr} (h : IsRE L) : MIPStarComputable L

RE ⊆ MIP*, conditionally on compression: the RE inclusion at the tensor-product model, with the halting reduction of cor:main-quantum.

theorem MIPRE.Halting.mipstarComputable_eq_re_of (G : GapCompression) (U : Cost.UniversalMachine) : MIPStarComputable = IsRE

MIP* = RE (blueprint thm:mipstar-eq-re), conditionally on compression: the two classes coincide, as predicates on languages.