Detyping with different answer alphabets

Soundness allows coarse-graining the detyped answers on the same state. The only predicate hypothesis is the required acceptance implication on valid questions; the longer-answer predicate may reject additional answers. This accounts for the cutoff/truncation distinction in types.tex.

noncomputable def MIPRE.CL.Detyping.restrictAnswers {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} {A' : Type u_5} {B' : Type u_6} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A'] [DecidableEq 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) (D' : Question T ι → Question T ι → A' → B' → Bool) (rA : Question T ι → A → A') (rB : Question T ι → B → B') (S : TensorProductStrategy (game E P D)) : TensorProductStrategy (typedGame E hne P D')

Restrict to typed views and merge answer outcomes, retaining the original state.

Equations

• MIPRE.CL.Detyping.restrictAnswers E hne P D D' rA rB S = S.adapt (MIPRE.CL.Detyping.typedGame E hne P D') (MIPRE.CL.Detyping.question E false) (MIPRE.CL.Detyping.question E true) rA rB

theorem MIPRE.CL.Detyping.restrictAnswers_state {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} {A' : Type u_5} {B' : Type u_6} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A'] [DecidableEq 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) (D' : Question T ι → Question T ι → A' → B' → Bool) (rA : Question T ι → A → A') (rB : Question T ι → B → B') (S : TensorProductStrategy (game E P D)) : (restrictAnswers E hne P D D' rA rB S).ψ = S.ψ

Coarse-graining after restriction literally preserves the shared state.

theorem MIPRE.CL.Detyping.restrictAnswers_failAt_le {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} {A' : Type u_5} {B' : Type u_6} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A'] [DecidableEq 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) (D' : Question T ι → Question T ι → A' → B' → Bool) (rA : Question T ι → A → A') (rB : Question T ι → B → B') (S : TensorProductStrategy (game E P D)) (x y : Question T ι) (hxy : E x.1 y.1) (hD : ∀ (a : A) (b : B), D x y a b = true → D' x y (rA x a) (rB y b) = true) : (restrictAnswers E hne P D D' rA rB S).failAt x y ≤ (restrict E hne P D S).failAt x y

Acceptance-preserving answer maps cannot increase conditional failure on an edge.

theorem MIPRE.CL.Detyping.restrictAnswers_failure_le {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} {A' : Type u_5} {B' : Type u_6} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A'] [DecidableEq B'] {ℓ : ℕ} (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 → B → Bool) (D' : Question T ι → Question T ι → A' → B' → Bool) (rA : Question T ι → A → A') (rB : Question T ι → B → B') (hD : ∀ (x y : Question T ι), E x.1 y.1 → ∀ (a : A) (b : B), D x y a b = true → D' x y (rA x a) (rB y b) = true) (S : TensorProductStrategy (game E P D)) : 1 - (restrictAnswers E hne P D D' rA rB S).value ≤ 16 ^ Fintype.card T * (1 - S.value)

The same-state soundness factor survives answer truncation and cutoff rejections.

theorem MIPRE.CL.Detyping.restrictAnswers_value_ge {T : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} {A' : Type u_5} {B' : Type u_6} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype B] [Fintype A'] [Fintype B'] [DecidableEq A'] [DecidableEq B'] {ℓ : ℕ} (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 → B → Bool) (D' : Question T ι → Question T ι → A' → B' → Bool) (rA : Question T ι → A → A') (rB : Question T ι → B → B') (hD : ∀ (x y : Question T ι), E x.1 y.1 → ∀ (a : A) (b : B), D x y a b = true → D' x y (rA x a) (rB y b) = true) (S : TensorProductStrategy (game E P D)) {ε : ℝ} (hS : 1 - ε ≤ S.value) : 1 - 16 ^ Fintype.card T * ε ≤ (restrictAnswers E hne P D D' rA rB S).value

A near-perfect longer-answer strategy yields the asserted shorter-answer strategy.