Documentation

MIPRE.Foundations.ValueModel

Value models: one interface for the tensor-product and the commuting-operator value #

The halting reduction of MIP* = RE and the one of MIP^co = coRE (planning/mipco-track.md) are the same argument in two values: val* (MIPRE.quantumValue) and the bipartite commuting-operator value ω_co (MIPRE.commutingOperatorValue). What the argument uses of the value is a short list — it is at most 1, it dominates the tensor-product value, and it is invariant under the presentations of a verifier's game that the reduction moves between: relabeling of the alphabets, padding of the answers by always-rejected ones, the doubled question set, and the frozen verifier — and the only place the two differ is the direction in which the value is semidecidable: val* from below (lem:value-lower-approx), ω_co from above (lem:valco-upper-re). ValueModel is that list, and the whole reduction is written once against it:

The universe of the alphabets is Type: the games of a verifier, their doubled forms and the tabulated games all live there, and the fields need no more.

source
theorem MIPRE.quantumValue_le_extendAnswers {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_1} {B' : Type u_2} [Fintype A'] [Fintype B'] (G : Game X Y A B) (G' : Game X Y A' B') (ιA : A ↪ A') (ιB : B ↪ B') (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G'.D x y (ιA a) (ιB b) = G.D x y a b) :
quantumValue G ≤ quantumValue G'

Enlarging the answer alphabets can only raise the quantum value: a strategy extends by zero operators on the new answers.

source
theorem MIPRE.commutingOperatorValue_le_extendAnswers {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {A' : Type u_1} {B' : Type u_2} [Fintype A'] [Fintype B'] (G : Game X Y A B) (G' : Game X Y A' B') (ιA : A ↪ A') (ιB : B ↪ B') (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y) (a : A) (b : B), G'.D x y (ιA a) (ιB b) = G.D x y a b) :
commutingOperatorValue G ≤ commutingOperatorValue G'

Enlarging the answer alphabets can only raise the commuting-operator value.

source
structure MIPRE.ValueModel :
Type 1

A value model: a value functional val on finite games — for val* and for ω_co, the supremum of the value of a strategy over a class of strategies — together with the properties of it that the halting reduction uses. The value is at most 1 and dominates the tensor-product value (every model contains the tensor-product strategies), and it is invariant under relabeling of the alphabets, monotone in the decision predicate, 0 on a game that rejects everything, unchanged by padding the answer alphabets with always-rejected answers, and unchanged by the doubling of the question set.

Instances For
    source
    theorem MIPRE.ValueModel.nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (ω : ValueModel) (G : Game X Y A B) :
    0 ≤ ω.val G

    The value is nonnegative: it dominates the tensor-product value.

    The two models #

    source
    noncomputable def MIPRE.ValueModel.tensor :
    ValueModel

    The tensor-product model: val*, the quantum value.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem MIPRE.ValueModel.tensor_val {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) :
      tensor.val G = quantumValue G
      source
      noncomputable def MIPRE.ValueModel.commuting :
      ValueModel

      The commuting-operator model: ω_co, the bipartite commuting-operator value.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem MIPRE.ValueModel.commuting_val {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) :
        commuting.val G = commutingOperatorValue G

        Semidecidability of the value, and the two shapes of a halting reduction #

        source
        def MIPRE.ValueModel.LowerRE (ω : ValueModel) :
        Prop

        The value is r.e. from below: the triples (d, p, q) with p / q < val(G_d) form an r.e. set, in the threshold encoding of lem:value-lower-approx (p / 0 = 0). The tensor-product model has it (ValueModel.tensor_lowerRE); the commuting-operator model does not, by MIP^co = coRE itself.

        Equations
        Instances For
          source
          def MIPRE.ValueModel.UpperRE (ω : ValueModel) :
          Prop

          The value is r.e. from above: the triples (d, p, q) with val(G_d) < p / q form an r.e. set. The commuting-operator model has it (ValueModel.commuting_upperRE, blueprint lem:valco-upper-re); the tensor-product model does not, by MIP* = RE itself.

          Equations
          Instances For
            source
            def MIPRE.ValueModel.HaltingReductionRE (ω : ValueModel) :
            Prop

            A halting reduction to the value, RE shape: a computable map from codes to game descriptions whose value is 1 on codes that halt on the empty input and at most 1/2 on the others. At tensor this is cor:main-quantum.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def MIPRE.ValueModel.HaltingReductionCoRE (ω : ValueModel) :
              Prop

              A halting reduction to the value, coRE shape: a computable map from codes to game descriptions whose value is at most 1/2 on codes that halt on the empty input and 1 on the others. At commuting this is thm:halting-co.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For