Documentation

MIPRE.Tailored.Class

The class TMIP*, and TMIP* = RE from tailored compression #

Paper II, II:787 and II:6997: the class reading of thm:tailored_MIP*=RE, as Foundations/ClassMIPStarComputable.lean and Halting/Corollaries.lean give it for MIP*.

The plan had TMIP* ⊆ RE by enumerating signed-permutation strategies, on which perfection is decidable. The route through the quantum value needs no new semidecider: the class's soundness clause is in the quantum value, so membership is val* > 1/2.

source
def MIPRE.Tailored.TMIPStarComputable (L : Set Cost.BitStr) :
Prop

TMIP*, computable version (II:787): a language L is in TMIPStarComputable if there is a computable map from strings to tailored game descriptions whose game has a perfect ZPC strategy when x ∈ L and quantum value at most 1/2 when x ∉ L.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.Tailored.TMIPStarComputable.mipStar {L : Set Cost.BitStr} (h : TMIPStarComputable L) :
    MIPStarComputable L

    TMIP* ⊆ MIP*: a perfect ZPC strategy gives value 1, and a tailored game description converts computably to a game description with the same quantum value.

    source
    theorem MIPRE.Tailored.TMIPStarComputable.isRE {L : Set Cost.BitStr} (h : TMIPStarComputable L) :
    IsRE L

    TMIP* ⊆ RE (II:1838), unconditionally.

    source
    theorem MIPRE.Tailored.re_subset_tmipStarComputable_of {ℓ : ℕ} (TG : TailoredGapCompression ℓ) {L : Set Cost.BitStr} (h : IsRE L) :
    TMIPStarComputable L

    RE ⊆ TMIP*, from a tailored gap compression.

    source
    theorem MIPRE.Tailored.tmipStarComputable_eq_re_of {ℓ : ℕ} (TG : TailoredGapCompression ℓ) :
    TMIPStarComputable = IsRE

    TMIP* = RE (II:787, II:6997), from a tailored gap compression: the two classes coincide, as predicates on languages.