Extending a tailored game along an embedding of its questions

A tailored game G' on X' extends a tailored game G on X along an embedding e : X ↪ X' (TailoredGame.Extends) when it has the weights, the lengths and the constraints of G on the image of e, and no weight off it. This is how the game of a polynomial-time tailored verifier on an input, whose questions are the strings of length at most B, relates to the game of the tailored verifier it simulates, whose questions are the vectors of 𝔽₂^s (MIPRE/Tailored/ClassVerifier.lean).

• Extends.valStar_eq: the two games have the same quantum value. Restricting G' to the image changes nothing, the distribution being supported there (quantumValue_restrictQuestions); the answers of length at most G.maxLen then sit inside those of length at most G'.maxLen, and the canonical decider rejects the longer ones (quantumValue_extendAnswers).
• Extends.hasPerfectZPC: a perfect ZPC strategy of G gives one of G', with its observables on the image and identities off it, where no question is asked: the strategy pulled back along the inverse of e (PermStrategy.comap, Tailored/Repeat/Strategy.lean).
• Extends.doubled: the doubled games extend each other along Bool × e, so the completeness clause of TMIP*, read on the doubled game, transfers too.

structure MIPRE.Tailored.TailoredGame.Extends {X : Type u_1} {X' : Type u_2} [Fintype X] [Fintype X'] (G' : TailoredGame X') (G : TailoredGame X) (e : X ↪ X') : Prop

G' extends G along e: the weights, the lengths and the constraints of G on the image of e, and no weight off it.

• μ_eq (x y : X) : G'.μ (e x) (e y) = G.μ x y
• support (x' y' : X') : G'.μ x' y' ≠ 0 → (∃ (x : X), e x = x') ∧ ∃ (y : X), e y = y'
• lenR_eq (x : X) : G'.lenR (e x) = G.lenR x
• lenL_eq (x : X) : G'.lenL (e x) = G.lenL x
• cons_eq (x y : X) : G'.cons (e x) (e y) = G.cons x y

theorem MIPRE.Tailored.TailoredGame.nonempty {X : Type u_1} [Fintype X] (G : TailoredGame X) : Nonempty X

A tailored game has a question: its weights sum to 1.

theorem MIPRE.Tailored.TailoredGame.Extends.len_eq {X : Type u_1} {X' : Type u_2} [Fintype X] [Fintype X'] {G' : TailoredGame X'} {G : TailoredGame X} {e : X ↪ X'} (h : G'.Extends G e) (x : X) : G'.len (e x) = G.len x

theorem MIPRE.Tailored.TailoredGame.Extends.accepts_iff {X : Type u_1} {X' : Type u_2} [Fintype X] [Fintype X'] {G' : TailoredGame X'} {G : TailoredGame X} {e : X ↪ X'} (h : G'.Extends G e) (x y : X) (a b : Cost.BitStr) : G'.Accepts (e x) (e y) a b ↔ G.Accepts x y a b

The canonical deciders agree on the image.

theorem MIPRE.Tailored.TailoredGame.Extends.maxLen_le {X : Type u_1} {X' : Type u_2} [Fintype X] [Fintype X'] {G' : TailoredGame X'} {G : TailoredGame X} {e : X ↪ X'} (h : G'.Extends G e) : G.maxLen ≤ G'.maxLen

The quantum value

theorem MIPRE.Tailored.TailoredGame.Extends.valStar_eq {X : Type u_1} {X' : Type u_2} [Fintype X] [Fintype X'] {G' : TailoredGame X'} {G : TailoredGame X} {e : X ↪ X'} (h : G'.Extends G e) : G'.valStar = G.valStar

The quantum value is that of G.

Perfect ZPC strategies

theorem MIPRE.Tailored.TailoredGame.Extends.hasPerfectZPC {X : Type u_1} {X' : Type u_2} [Fintype X] [Fintype X'] {G' : TailoredGame X'} {G : TailoredGame X} {e : X ↪ X'} (h : G'.Extends G e) (hG : G.HasPerfectZPC) : G'.HasPerfectZPC

A perfect ZPC strategy of G gives one of G': the strategy pulled back along the inverse of e (PermStrategy.comap), with its observables at the questions of the image and identities elsewhere.

The doubled games

theorem MIPRE.Tailored.TailoredGame.Extends.doubled {X : Type u_1} {X' : Type u_2} [Fintype X] [Fintype X'] {G' : TailoredGame X'} {G : TailoredGame X} {e : X ↪ X'} (h : G'.Extends G e) : G'.doubled.Extends G.doubled ((Function.Embedding.refl Bool).prodMap e)

The doubled games extend each other along Bool × e.