PCC completeness of finite-game detyping

The complete strategy uses the input strategy's dimension and one common measurement rule for both players. Invalid local graph views select a constant measurement. On jointly valid views, the original strategy is played on the same ordered edge and common content seed.

theorem MIPRE.CL.Detyping.sample_dist_pos_iff {S : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype S] [Nonempty S] [Fintype X] [Fintype Y] (qA : S → X) (qB : S → Y) (x : X) (y : Y) : 0 < SampledGame.dist qA qB x y ↔ ∃ (s : S), qA s = x ∧ qB s = y

theorem MIPRE.CL.Detyping.sample_failAt_zero {U : Type u_1} {X : Type u_2} {Y : Type u_3} {A : Type u_4} {B : Type u_5} [Fintype U] [Nonempty U] [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (qA : U → X) (qB : U → Y) (D : X → Y → A → B → Bool) (S : TensorProductStrategy (SampledGame.game qA qB D)) (hS : S.value = 1) (u : U) : S.failAt (qA u) (qB u) = 0

theorem MIPRE.CL.Detyping.failAt_zero_of_accepts {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) (x : X) (y : Y) (h : ∀ (a : A) (b : B), G.D x y a b = true) : S.failAt x y = 0

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

The input measurements on decoded questions, with a deterministic fallback. The outer doubling tag is ignored, so both players use literally the same rule.

Equations

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

theorem MIPRE.CL.Detyping.complete_state {T : Type u_1} {ι : Type u_2} {A : Type u_3} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → A → Bool) (S : SyncStrategy (typedGame E hne P D).doubled) (a₀ : A) : (complete E hne P D S a₀).toTensorProductStrategy.undouble.ψ = S.toTensorProductStrategy.undouble.ψ

The canonical tensor realizations use literally the same shared state.

theorem MIPRE.CL.Detyping.complete_player_independent {T : Type u_1} {ι : Type u_2} {A : Type u_3} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → A → Bool) (S : SyncStrategy (typedGame E hne P D).doubled) (a₀ : A) (q : Coord T ι → ZMod 2) (a : A) : (complete E hne P D S a₀).P.M (false, q) a = (complete E hne P D S a₀).P.M (true, q) a

Both tagged players use the same measurement on every question, including invalid ones.

theorem MIPRE.CL.Detyping.complete_M_question {T : Type u_1} {ι : Type u_2} {A : Type u_3} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → A → Bool) (S : SyncStrategy (typedGame E hne P D).doubled) (a₀ : A) (tag w : Bool) (q : Question T ι) (a : A) : (complete E hne P D S a₀).P.M (tag, question E w q) a = S.P.M (w, q) a

On every valid view the common measurement rule is the original typed rule.

theorem MIPRE.CL.Detyping.typed_mu_pos {T : Type u_1} {ι : Type u_2} {A : Type u_3} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → A → Bool) {u v : T} (huv : E u v) (z : ι → ZMod 2) : 0 < (typedGame E hne P D).μ (u, (P false u).eval z) (v, (P true v).eval z)

The typed distribution gives positive mass to every edge and content seed.

theorem MIPRE.CL.Detyping.complete_commutes_sample {T : Type u_1} {ι : Type u_2} {A : Type u_3} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (D : Question T ι → Question T ι → A → A → Bool) (S : SyncStrategy (typedGame E hne P D).doubled) (hS : S.IsPCC) (a₀ : A) (g : Graph.Coord T → ZMod 2) (z : ι → ZMod 2) (a b : A) : have R := complete E hne P D S a₀; have x := (presentation E false (P false)).eval (Sum.elim g z); have y := (presentation E true (P true)).eval (Sum.elim g z); R.P.M (false, x) a * R.P.M (true, y) b = R.P.M (true, y) b * R.P.M (false, x) a

At each detyped seed, the two measurements commute if the original strategy is PCC.

theorem MIPRE.CL.Detyping.complete_isPCC {T : Type u_1} {ι : Type u_2} {A : Type u_3} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (D : Question T ι → Question T ι → A → A → Bool) (S : SyncStrategy (typedGame E hne P D).doubled) (hS : S.IsPCC) (a₀ : A) : (complete E hne P D S a₀).IsPCC

The completed strategy is PCC on the entire support of the detyped game.

theorem MIPRE.CL.Detyping.accepts_sample_of_none {T : Type u_1} {ι : Type u_2} {A : Type u_3} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (D : Question T ι → Question T ι → A → A → Bool) (g : Graph.Coord T → ZMod 2) (z : ι → ZMod 2) (h : select E false g = none ∨ select E true g = none) (a b : A) : accepts E D ((presentation E false (P false)).eval (Sum.elim g z)) ((presentation E true (P true)).eval (Sum.elim g z)) a b = true

If a player has an invalid local sample, the detyped predicate always accepts.

theorem MIPRE.CL.Detyping.complete_failAt_question {T : Type u_1} {ι : Type u_2} {A : Type u_3} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (D : Question T ι → Question T ι → A → A → Bool) (S : SyncStrategy (typedGame E hne P D).doubled) (a₀ : A) (x y : Question T ι) (hxy : E x.1 y.1) : (complete E hne P D S a₀).toTensorProductStrategy.undouble.failAt (question E false x) (question E true y) = S.toTensorProductStrategy.undouble.failAt x y

On valid views the completed strategy has exactly the original conditional failure.

theorem MIPRE.CL.Detyping.complete_failAt_sample {T : Type u_1} {ι : Type u_2} {A : Type u_3} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (D : Question T ι → Question T ι → A → A → Bool) (S : SyncStrategy (typedGame E hne P D).doubled) (hval : S.value = 1) (a₀ : A) (g : Graph.Coord T → ZMod 2) (z : ι → ZMod 2) : (complete E hne P D S a₀).toTensorProductStrategy.undouble.failAt ((presentation E false (P false)).eval (Sum.elim g z)) ((presentation E true (P true)).eval (Sum.elim g z)) = 0

Every actual sample is won with certainty by completion of a perfect typed strategy.

theorem MIPRE.CL.Detyping.complete_value {T : Type u_1} {ι : Type u_2} {A : Type u_3} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (D : Question T ι → Question T ι → A → A → Bool) (S : SyncStrategy (typedGame E hne P D).doubled) (hval : S.value = 1) (a₀ : A) : (complete E hne P D S a₀).value = 1

Completion preserves perfect value.

theorem MIPRE.CL.Detyping.exists_perfectPCC {T : Type u_1} {ι : Type u_2} {A : Type u_3} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (D : Question T ι → Question T ι → A → A → Bool) (S : SyncStrategy (typedGame E hne P D).doubled) (hS : S.IsPCC) (hval : S.value = 1) (a₀ : A) : ∃ (R : SyncStrategy (game E P D).doubled), R.IsPCC ∧ R.value = 1 ∧ R.d = S.d

Finite-game detyping preserves a perfect PCC witness and its dimension.