A tailored game description presenting a tailored game

A TailoredGameValue.TailoredGameData presents a tailored game G of the library (MIPRE.Tailored.TailoredGame) along a bijection e of its vertices with G's questions when it has the same weights, the same numbers of readable and linear variables, and the same constraints (Presents). The two read answers differently — the description reads bit vectors of the largest length that vanish beyond a vertex's variables, the library bit strings of exactly that length — and the description's canonical decider also rejects unequal answers at a loop. On a game with no weight on its loops, such as a doubled game, neither difference costs anything:

• Presents.quantumValue_eq: the description has the quantum value of the game. Answers pass from vectors to strings by keeping a vertex's coordinates (Presents.toStr) and back by padding with zeros (Presents.toVec), question by question (TensorProductStrategy.mergeAnswersByQuestion).
• Presents.hasPerfectZPC: a perfect ZPC strategy of the game is one of the description, its observables padded with identities.

Two general facts are used: the quantum value depends on the decision predicate only where the distribution has weight (quantumValue_eq_of_equiv_support), and a tailored game and its doubled game have the same quantum value (TailoredGame.quantumValue_doubled_eq_valStar).

The quantum value sees the predicate only where there is weight

theorem MIPRE.TensorProductStrategy.value_copy_support {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : TensorProductStrategy G) (G' : Game X Y A B) (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y), G.μ x y ≠ 0 → ∀ (a : A) (b : B), G'.D x y a b = G.D x y a b) : (S.copy G').value = S.value

Strategies have the same value on two games with the same distribution and predicates that agree wherever the distribution has weight.

theorem MIPRE.quantumValue_congr_support {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G G' : Game X Y A B) (hμ : ∀ (x : X) (y : Y), G'.μ x y = G.μ x y) (hD : ∀ (x : X) (y : Y), G.μ x y ≠ 0 → ∀ (a : A) (b : B), G'.D x y a b = G.D x y a b) : quantumValue G' = quantumValue G

The quantum value depends on the predicate only where the distribution has weight.

theorem MIPRE.quantumValue_eq_of_equiv_support {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {X' : Type u_5} {Y' : Type u_6} {A' : Type u_7} {B' : Type u_8} [Fintype X'] [Fintype Y'] [Fintype A'] [Fintype B'] (G : Game X Y A B) (G' : Game X' Y' A' B') (eX : X' ≃ X) (eY : Y' ≃ Y) (eA : A' ≃ A) (eB : B' ≃ B) (hμ : ∀ (x' : X') (y' : Y'), G'.μ x' y' = G.μ (eX x') (eY y')) (hD : ∀ (x' : X') (y' : Y'), G'.μ x' y' ≠ 0 → ∀ (a' : A') (b' : B'), G'.D x' y' a' b' = G.D (eX x') (eY y') (eA a') (eB b')) : quantumValue G' = quantumValue G

Relabeling, with the predicates agreeing only where there is weight.

theorem MIPRE.TensorProductStrategy.value_le_mergeAnswersByQuestion' {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {A' : Type u_5} {B' : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A] [DecidableEq B] {G' : Game X Y A' B'} (S' : TensorProductStrategy G') (G : Game X Y A B) (rA : X → A' → A) (rB : Y → 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' b' = true → G.D x y (rA x a') (rB y b') = true) : S'.value ≤ (S'.mergeAnswersByQuestion G rA rB).value

Question-dependent answer decoding can only raise the value of a tensor-product strategy.

theorem MIPRE.Tailored.TailoredGame.doubled_μ_self {X : Type u_1} [Fintype X] (G : TailoredGame X) (p : Bool × X) : G.doubled.μ p p = 0

The doubled game has no weight on its loops.

theorem MIPRE.Tailored.TailoredGame.doubled_maxLen {X : Type u_1} [Fintype X] (G : TailoredGame X) : G.doubled.maxLen = G.maxLen

theorem MIPRE.Tailored.TailoredGame.quantumValue_doubled_eq_valStar {X : Type u_1} [Fintype X] (G : TailoredGame X) : quantumValue G.doubled.toGame = G.valStar

A tailored game and its doubled game have the same quantum value.

Fourier transforms padded with identities

theorem MIPRE.Tailored.fourierFactor_one_false {R : Type u_1} [Ring R] [Algebra ℂ R] : fourierFactor 1 false = 1

theorem MIPRE.Tailored.fourierFactor_one_true {R : Type u_1} [Ring R] [Algebra ℂ R] : fourierFactor 1 true = 0

theorem MIPRE.Tailored.fourierProj_eq_zero_of_one {R : Type u_1} [Ring R] [Algebra ℂ R] {n : ℕ} (U : Fin n → R) (a : Fin n → Bool) (k : Fin n) (hU : U k = 1) (ha : a k = true) : fourierProj U a = 0

An observable equal to the identity annihilates the Fourier transform at an answer whose bit there is 1.

theorem MIPRE.Tailored.fourierProj_castLE {R : Type u_1} [Ring R] [Algebra ℂ R] {L n : ℕ} (hL : L ≤ n) (U : Fin n → R) (hU : ∀ (k : Fin n), L ≤ ↑k → U k = 1) (a : Fin n → Bool) (ha : ∀ (k : Fin n), L ≤ ↑k → a k = false) : fourierProj U a = fourierProj (fun (k : Fin L) => U (Fin.castLE hL k)) fun (k : Fin L) => a (Fin.castLE hL k)

Padding with identities: observables equal to the identity beyond L leave the Fourier transform unchanged at an answer that vanishes beyond L.

Presentations

structure MIPRE.Tailored.Presents {X : Type u_1} [Fintype X] (g : TailoredGameValue.TailoredGameData) (G : TailoredGame X) (e : Fin (g.nV + 1) ≃ X) : Prop

A tailored game description presents a tailored game along a bijection of its vertices with the game's questions: the same weights, the same numbers of readable and linear variables, and, for every pair of vertices and every readable part of the right length, the same constraints.

• μ_eq (i j : Fin (g.nV + 1)) : g.toGame.μ i j = G.μ (e i) (e j)
• lenR_eq (i : Fin (g.nV + 1)) : g.lenRAt ↑i = G.lenR (e i)
• lenL_eq (i : Fin (g.nV + 1)) : g.lenLAt ↑i = G.lenL (e i)
• cons_iff (i j : Fin (g.nV + 1)) (γ c : List Bool) : γ.length = G.lenR (e i) + G.lenR (e j) → ((↑i, ↑j, γ, c) ∈ g.cons ↔ c ∈ G.cons (e i) (e j) (List.take (G.lenR (e i)) γ) (List.drop (G.lenR (e i)) γ))

theorem MIPRE.Tailored.Presents.lenAt_eq {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (i : Fin (g.nV + 1)) : g.lenAt ↑i = G.len (e i)

theorem MIPRE.Tailored.Presents.length_full {g : TailoredGameValue.TailoredGameData} (i : Fin (g.nV + 1)) (a : Fin g.ansLen → Bool) : (g.full i a).length = g.lenAt ↑i

theorem MIPRE.Tailored.Presents.readable_eq_take {g : TailoredGameValue.TailoredGameData} (i : Fin (g.nV + 1)) (a : Fin g.ansLen → Bool) : g.readable i a = List.take (g.lenRAt ↑i) (g.full i a)

def MIPRE.Tailored.Presents.toStr {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (i : Fin (g.nV + 1)) (a : Fin g.ansLen → Bool) : Verifier.Answers G.maxLen

The answer at vertex i, as the bit string of its variables.

Equations

• hP.toStr i a = ⟨g.full i a, ⋯⟩

def MIPRE.Tailored.Presents.toVec {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} (s : Verifier.Answers G.maxLen) : Fin g.ansLen → Bool

A bit string, as an answer vector: padded with zeros, truncated at the largest length.

Equations

• MIPRE.Tailored.Presents.toVec s k = List.getD (↑s) (↑k) false

theorem MIPRE.Tailored.Presents.full_toVec {g : TailoredGameValue.TailoredGameData} (i : Fin (g.nV + 1)) (s : Cost.BitStr) (hs : List.length s = g.lenAt ↑i) : (g.full i fun (k : Fin g.ansLen) => List.getD s (↑k) false) = s

theorem MIPRE.Tailored.Presents.wellFormatted_toVec {g : TailoredGameValue.TailoredGameData} (i : Fin (g.nV + 1)) (s : Cost.BitStr) (hs : List.length s = g.lenAt ↑i) : g.WellFormatted i fun (k : Fin g.ansLen) => List.getD s (↑k) false

theorem MIPRE.Tailored.Presents.accepts_iff {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (i j : Fin (g.nV + 1)) (a b : Fin g.ansLen → Bool) (ha : g.WellFormatted i a) (hb : g.WellFormatted j b) : g.Accepts i j a b ↔ (i = j → a = b) ∧ G.Accepts (e i) (e j) (g.full i a) (g.full j b)

The two deciders agree on well-formatted answers: the description's accepts exactly when the answers are equal at a loop and the game accepts their bit strings.

The quantum value

noncomputable def MIPRE.Tailored.Presents.midGame {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} : Game (Fin (g.nV + 1)) (Fin (g.nV + 1)) (Verifier.Answers G.maxLen) (Verifier.Answers G.maxLen)

The game on the description's vertices with the library's answers: the game read along e, rejecting unequal answers at a loop.

Equations

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

theorem MIPRE.Tailored.Presents.quantumValue_midGame {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (hloop : ∀ (x : X), G.μ x x = 0) : quantumValue midGame = quantumValue G.toGame

theorem MIPRE.Tailored.Presents.quantumValue_le_midGame {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) : quantumValue g.game ≤ quantumValue midGame

theorem MIPRE.Tailored.Presents.midGame_le_quantumValue {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) : quantumValue midGame ≤ quantumValue g.game

theorem MIPRE.Tailored.Presents.quantumValue_eq {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (hloop : ∀ (x : X), G.μ x x = 0) : quantumValue g.game = quantumValue G.toGame

A presentation of a game with no weight on its loops has the game's quantum value.

Perfect ZPC strategies

theorem MIPRE.Tailored.Presents.len_le_ansLen {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (i : Fin (g.nV + 1)) : G.len (e i) ≤ g.ansLen

def MIPRE.Tailored.Presents.padVec {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} (G : TailoredGame X) (e : Fin (g.nV + 1) ≃ X) (i : Fin (g.nV + 1)) (a : Fin (G.len (e i)) → Bool) : Fin g.ansLen → Bool

An answer to a question, as an answer vector at its vertex: padded with zeros.

Equations

• MIPRE.Tailored.Presents.padVec G e i a k = if h : ↑k < G.len (e i) then a ⟨↑k, h⟩ else false

theorem MIPRE.Tailored.Presents.padVec_injective {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (i : Fin (g.nV + 1)) : Function.Injective (padVec G e i)

theorem MIPRE.Tailored.Presents.exists_of_not_mem_range {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (i : Fin (g.nV + 1)) (a : Fin g.ansLen → Bool) (ha : a ∉ Set.range (padVec G e i)) : ∃ (k : Fin g.ansLen), G.len (e i) ≤ ↑k ∧ a k = true

An answer vector that is not padded has a 1 beyond the question's variables.

theorem MIPRE.Tailored.Presents.wellFormatted_padVec {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (i : Fin (g.nV + 1)) (a : Fin (G.len (e i)) → Bool) : g.WellFormatted i (padVec G e i a)

theorem MIPRE.Tailored.Presents.full_padVec {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (i : Fin (g.nV + 1)) (a : Fin (G.len (e i)) → Bool) : g.full i (padVec G e i a) = List.ofFn a

noncomputable def MIPRE.Tailored.Presents.padStrategy {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (S : PermStrategy G) : TailoredGameValue.PermStrategy g

The padded strategy: a permutation strategy of the game, read on the description, its observables padded with identities beyond a question's variables.

Equations

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

theorem MIPRE.Tailored.Presents.proj_padStrategy_eq_zero {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (S : PermStrategy G) (i : Fin (g.nV + 1)) (a : Fin g.ansLen → Bool) (k : Fin g.ansLen) (hk : G.len (e i) ≤ ↑k) (ha : a k = true) : (hP.padStrategy S).proj i a = 0

The padded strategy's measurement at an unpadded answer vector is 0.

theorem MIPRE.Tailored.Presents.proj_padStrategy {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (S : PermStrategy G) (i : Fin (g.nV + 1)) (a : Fin (G.len (e i)) → Bool) : (hP.padStrategy S).proj i (padVec G e i a) = S.proj (e i) a

The padded strategy's measurement at a padded answer is the strategy's.

theorem MIPRE.Tailored.Presents.value_padStrategy {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (hloop : ∀ (x : X), G.μ x x = 0) (S : PermStrategy G) : (hP.padStrategy S).value = S.value

The padded strategy has the strategy's value, on a game with no weight on its loops.

theorem MIPRE.Tailored.Presents.hasPerfectZPC {X : Type u_1} [Fintype X] {g : TailoredGameValue.TailoredGameData} {G : TailoredGame X} {e : Fin (g.nV + 1) ≃ X} (hP : Presents g G e) (hloop : ∀ (x : X), G.μ x x = 0) (h : G.HasPerfectZPC) : g.HasPerfectZPC

A perfect ZPC strategy of a game with no weight on its loops is one of a presentation.