The finite typed and detyped games

This is the game at a fixed verifier index, before ambient-program compilation. The detyped predicate accepts outside valid edge views. On valid views it calls the original predicate. The answer alphabets here are unchanged; the separate program-level cutoff and answer truncation obligations are not hidden here.

theorem MIPRE.CL.Detyping.sampled_dist_cl {J : Type u_1} [Fintype J] [DecidableEq J] (L R : (J → ZMod 2) → J → ZMod 2) (x y : J → ZMod 2) : SampledGame.dist L R x y = clDist L R x y

@[reducible, inline]

abbrev MIPRE.CL.Detyping.Question (T : Type u_5) (ι : Type u_6) : Type (max u_5 u_6)

Typed questions carry a type and its sampled content.

Equations

• MIPRE.CL.Detyping.Question T ι = (T × (ι → ZMod 2))

def MIPRE.CL.Detyping.question {T : Type u_1} {ι : Type u_2} [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (q : Question T ι) : Coord T ι → ZMod 2

Embed a typed question using the type's fixed local graph view.

Equations

• MIPRE.CL.Detyping.question E w q = Sum.elim (MIPRE.CL.Detyping.view E w q.1) q.2

theorem MIPRE.CL.Detyping.select_view {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (u : T) : select E w (view E w u) = some u

A valid graph view decodes to its type.

theorem MIPRE.CL.Detyping.view_disjoint {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (u v : T) : view E false u ≠ view E true v

The two players' families of valid graph views are disjoint.

noncomputable def MIPRE.CL.Detyping.accepts {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (D : Question T ι → Question T ι → A → B → Bool) (x y : Coord T ι → ZMod 2) (a : A) (b : B) : Bool

The detyped predicate: call the typed predicate on an edge view, otherwise accept.

Equations

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

theorem MIPRE.CL.Detyping.accepts_question {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] (E : T → T → Prop) [DecidableRel E] (D : Question T ι → Question T ι → A → B → Bool) (x y : Question T ι) (h : E x.1 y.1) (a : A) (b : B) : accepts E D (question E false x) (question E true y) a b = D x y a b

On an edge, the fixed graph views make the detyped predicate exactly the typed one.

@[reducible, inline]

abbrev MIPRE.CL.Detyping.Edge {T : Type u_1} [Fintype T] (E : T → T → Prop) [DecidableRel E] : Type u_1

Ordered adjacent pairs, including loops.

Equations

• MIPRE.CL.Detyping.Edge E = ↥(MIPRE.CL.Graph.edges E)

@[reducible, inline]

abbrev MIPRE.CL.Detyping.TypedSeed {T : Type u_1} [Fintype T] (E : T → T → Prop) [DecidableRel E] (ι : Type u_5) : Type (max u_1 u_5)

The typed sample space is an ordered edge together with one common content seed.

Equations

• MIPRE.CL.Detyping.TypedSeed E ι = (MIPRE.CL.Detyping.Edge E × (ι → ZMod 2))

def MIPRE.CL.Detyping.typedQuestion {T : Type u_1} {ι : Type u_2} [Fintype T] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {E : T → T → Prop} [DecidableRel E] (P : Bool → T → CLFun (ZMod 2) ι ℓ) (w : Bool) (z : TypedSeed E ι) : Question T ι

One player's typed question from an edge and common seed.

Equations

• MIPRE.CL.Detyping.typedQuestion P w z = (if w = true then (↑z.1).2 else (↑z.1).1, (P w (if w = true then (↑z.1).2 else (↑z.1).1)).eval z.2)

noncomputable def MIPRE.CL.Detyping.typedGame {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → B → Bool) : Game (Question T ι) (Question T ι) A B

The actual finite typed game, sampling a uniform ordered edge and common seed.

Equations

• MIPRE.CL.Detyping.typedGame E hne P D = MIPRE.SampledGame.game (MIPRE.CL.Detyping.typedQuestion P false) (MIPRE.CL.Detyping.typedQuestion P true) D

noncomputable def MIPRE.CL.Detyping.game {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → B → Bool) : Game (Coord T ι → ZMod 2) (Coord T ι → ZMod 2) A B

The actual finite detyped game, using the constructed CL presentations.

Equations

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

theorem MIPRE.CL.Detyping.game_mu_eq_clDist {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → B → Bool) (x y : Coord T ι → ZMod 2) : (game E P D).μ x y = clDist (presentation E false (P false)).eval (presentation E true (P true)).eval x y

The finite game's law is the library's CL distribution of the constructed presentations.

noncomputable def MIPRE.CL.Detyping.restrict {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → B → Bool) (S : TensorProductStrategy (game E P D)) : TensorProductStrategy (typedGame E hne P D)

Restrict the strategy's measurements to fixed graph views; its state and dimensions persist.

Equations

• MIPRE.CL.Detyping.restrict E hne P D S = S.relabel (MIPRE.CL.Detyping.typedGame E hne P D) (MIPRE.CL.Detyping.question E false) (MIPRE.CL.Detyping.question E true) (Equiv.refl A) (Equiv.refl B)

theorem MIPRE.CL.Detyping.restrict_state {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → B → Bool) (S : TensorProductStrategy (game E P D)) : (restrict E hne P D S).ψ = S.ψ

Restriction literally preserves the shared state.

theorem MIPRE.CL.Detyping.restrict_failAt {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → B → Bool) (S : TensorProductStrategy (game E P D)) (x y : Question T ι) (h : E x.1 y.1) : (restrict E hne P D S).failAt x y = S.failAt (question E false x) (question E true y)

Conditional failure agrees on every edge, with no change of state.

theorem MIPRE.CL.Detyping.typed_failure {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → B → Bool) (S : TensorProductStrategy (typedGame E hne P D)) : 1 - S.value = (∑ uv ∈ Graph.edges E, ∑ v : ι → ZMod 2, S.failAt (uv.1, (P false uv.1).eval v) (uv.2, (P true uv.2).eval v)) / (↑(Graph.edges E).card * ↑(Fintype.card (ι → ZMod 2)))

The typed failure is the uniform edge-and-content average of the restricted failures.

theorem MIPRE.CL.Detyping.failure {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → B → Bool) (S : TensorProductStrategy (game E P D)) : 1 - S.value = (∑ g : Graph.Coord T → ZMod 2, ∑ v : ι → ZMod 2, S.failAt ((presentation E false (P false)).eval (Sum.elim g v)) ((presentation E true (P true)).eval (Sum.elim g v))) / (16 ^ Fintype.card T * ↑(Fintype.card (ι → ZMod 2)))

The detyped failure is the uniform average over its independent graph and content seeds.