Documentation

MIPRE.Background.Tailored.Main

TMIP* = RE from tailored answer reduction #

Phase 5 of planning/aldous-lyons-track.md. Question reduction (TailoredIntrospection 7, Intro.Inhabit.tailoredIntrospection) and parallel repetition (TailoredRepetition 7, tailoredRepetition) are inhabited, so TailoredGapCompression.ofTailoredPipeline turns a TailoredAnswerReduction 5 into a tailored gap compression, and the halting reduction of MIPRE/Tailored/Halting/ and the class theorem of MIPRE/Tailored/Class.lean follow from it: paper II's main theorem thm:tailored_MIP*=RE (II:1505) rests on answer reduction alone.

source
noncomputable def MIPRE.Tailored.TailoredGapCompression.ofAnswerReduction (A : TailoredAnswerReduction 5) :
TailoredGapCompression 7

Tailored compression from answer reduction: the composition with the inhabited question reduction and parallel repetition.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.Tailored.tailored_halting_reduction_of_answerReduction (A : TailoredAnswerReduction 5) :
    TailoredGameValue.TailoredHaltingReduction

    thm:tailored_MIP*=RE from tailored answer reduction (II:1505): a TailoredAnswerReduction 5 gives the halting reduction to tailored games.

    source
    theorem MIPRE.Tailored.tmipStarComputable_eq_re_of_answerReduction (A : TailoredAnswerReduction 5) :
    TMIPStarComputable = IsRE

    TMIP* = RE from tailored answer reduction (II:787, II:6997).