A tailored verifier extending a tailored game, from its programs

A tailored verifier W meets a tailored game G on X at an index n along an equivalence e : X ≃ 𝔽₂^{s(n)} of the questions (MeetsAt) when its sampler's distribution is G's weights along e, and at every question e x its answer-length calculator outputs G's lengths and its linear-constraints processor G's constraints. Then W's n-th game extends G along e (MeetsAt.extends), so it has G's quantum value (MeetsAt.valStar_eq) and its perfect ZPC strategies (MeetsAt.hasPerfectZPC).

This is the step from a game a stage presents to the output verifier of the stage, once the output's programs are shown to compute the presented lengths and constraints: the introspection stage proves it for its own presentation (Intro.Output.extends_presented), the answer reduction through this generic form.

theorem MIPRE.Tailored.TailoredVerifier.lenOf_eq_of_lenIs {ℓ : ℕ} (W : TailoredVerifier ℓ) (n : ℕ) {x : Cost.BitStr} {κ : Bool} {k : ℕ} (h : LenIs W.len n x κ k) : W.lenOf n x κ = k

structure MIPRE.Tailored.TailoredVerifier.MeetsAt {ℓ : ℕ} (W : TailoredVerifier ℓ) (n : ℕ) {X : Type u_1} [Fintype X] (G : TailoredGame X) (e : X ≃ W.Questions n) : Prop

W meets G at n along e: the sampler's distribution is G's weights, and the two programs output G's lengths and constraints at the questions e x.

• dist_eq (x y : X) : W.sampler.dist n (e x) (e y) = G.μ x y
• lenR_eq (x : X) : LenIs W.len n (CL.toBits (e x)) false (G.lenR x)
• lenL_eq (x : X) : LenIs W.len n (CL.toBits (e x)) true (G.lenL x)
• cons_eq (x y : X) (aR bR : Cost.BitStr) : LpIs W.lp n (CL.toBits (e x)) (CL.toBits (e y)) aR bR (G.cons x y aR bR)

theorem MIPRE.Tailored.TailoredVerifier.MeetsAt.extends_ {ℓ : ℕ} {W : TailoredVerifier ℓ} {n : ℕ} {X : Type u_1} [Fintype X] {G : TailoredGame X} {e : X ≃ W.Questions n} (h : W.MeetsAt n G e) : (W.tgame n).Extends G e.toEmbedding

W's n-th game extends G along e.

theorem MIPRE.Tailored.TailoredVerifier.MeetsAt.valStar_eq {ℓ : ℕ} {W : TailoredVerifier ℓ} {n : ℕ} {X : Type u_1} [Fintype X] {G : TailoredGame X} {e : X ≃ W.Questions n} (h : W.MeetsAt n G e) : W.valStar n = G.valStar

W's n-th game has G's quantum value.

theorem MIPRE.Tailored.TailoredVerifier.MeetsAt.hasPerfectZPC {ℓ : ℕ} {W : TailoredVerifier ℓ} {n : ℕ} {X : Type u_1} [Fintype X] {G : TailoredGame X} {e : X ≃ W.Questions n} (h : W.MeetsAt n G e) (hG : G.doubled.HasPerfectZPC) : W.HasPerfectZPC n

A perfect ZPC strategy of G's doubled game gives one of W's n-th game.