Documentation

MIPRE.Background.Pipeline

The pipeline with its supplied stages: MIP* = RE from answer reduction alone #

GapCompression.ofPipeline builds the compression theorem from three stage contracts: Introspection 7, AnswerReduction 5 and Repetition 7. Two of them are now inhabited:

A universal machine is supplied too (Cost.selfUniversal, blueprint lem:universal-tm). This file plugs all three in, so that every conditional consequence of chapter 7 — thm:main, cor:main-quantum, cor:value-uncomputable, thm:mipstar-eq-re — is stated with the single remaining hypothesis, an AnswerReduction 5.

The file compiling is the check that ofPipeline composes with Introspection.seven and repetition 7 as they are. The last hypothesis is supplied by AnswerReduction.answerReduction (MIPRE/Background/AnswerReduction/Instance.lean), and MIPRE/MainTheorem.lean proves the main theorem, HaltingGameValue.halting_reduces_to_gameValue, through halting_reduces_to_gameValue_of_answerReduction.

source
noncomputable def MIPRE.GapCompression.ofAnswerReduction (A : AnswerReduction 5) :
GapCompression

The compression theorem from answer reduction alone: GapCompression.ofPipeline with the supplied introspection and repetition stages.

Equations
Instances For
    source
    theorem MIPRE.Halting.halting_reduces_to_gameValue_of_answerReduction (A : AnswerReduction 5) :
    ∃ (g : Nat.Partrec.Code → HaltingGameValue.GameData), Computable g ∧ ∀ (pc : Nat.Partrec.Code), (HaltingGameValue.HaltsOnEmptyInput pc → HaltingGameValue.gameValue (g pc).toGame = 1) ∧ (¬HaltingGameValue.HaltsOnEmptyInput pc → HaltingGameValue.gameValue (g pc).toGame ≤ 1 / 2)

    Halting reduces to the synchronous game value (blueprint thm:main), conditionally on answer reduction only.

    source
    theorem MIPRE.Halting.halting_reduction_quantum_of_answerReduction (A : AnswerReduction 5) :
    ∃ (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), conditionally on answer reduction only.

    source
    theorem MIPRE.Halting.gameValue_uncomputable_of_answerReduction (A : AnswerReduction 5) :
    ¬∃ (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), conditionally on answer reduction only.

    source
    theorem MIPRE.Halting.quantumValue_uncomputable_of_answerReduction (A : AnswerReduction 5) :
    ¬∃ (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), conditionally on answer reduction only.

    source
    theorem MIPRE.Halting.re_subset_mipstarComputable_of_answerReduction (A : AnswerReduction 5) {L : Set Cost.BitStr} (h : IsRE L) :
    MIPStarComputable L

    RE ⊆ MIP*, conditionally on answer reduction only.

    source
    theorem MIPRE.Halting.mipstarComputable_eq_re_of_answerReduction (A : AnswerReduction 5) :
    MIPStarComputable = IsRE

    MIP* = RE (blueprint thm:mipstar-eq-re), conditionally on answer reduction only: introspection, parallel repetition and the universal machine are supplied.

    source
    theorem MIPRE.Halting.re_subset_mipstar_of_answerReduction (A : AnswerReduction 5) {L : Set Cost.BitStr} (h : IsRE L) :
    MIPStar L

    RE ⊆ MIP*_{1,1/2}(2,1), the paper's class, conditionally on answer reduction only.

    source
    theorem MIPRE.Halting.mipstar_eq_re_of_answerReduction (A : AnswerReduction 5) :
    MIPStar = IsRE

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