Perfect PCC strategies under question-dependent answer encoding #
Answers can be encoded separately at each question. The encoding need only preserve acceptance for nonzero effects on question pairs of positive weight. This allows format and range facts supplied by an honest strategy's support.
def
MIPRE.SyncStrategy.mergeAnswersByQuestion
{X : Type u_1}
{A : Type u_2}
{B : Type u_3}
[Fintype X]
[Fintype A]
[DecidableEq A]
[Fintype B]
[DecidableEq B]
{G : SynchronousGame X A}
(S : SyncStrategy G)
(H : SynchronousGame X B)
(f : X → A → B)
:
Group outcomes using the encoder appropriate to each question.
Equations
- S.mergeAnswersByQuestion H f = { d := S.d, d_pos := ⋯, P := S.P.mergeByQuestion f }
Instances For
theorem
MIPRE.SyncStrategy.isPCC_mergeAnswersByQuestion
{X : Type u_1}
{A : Type u_2}
{B : Type u_3}
[Fintype X]
[Fintype A]
[DecidableEq A]
[Fintype B]
[DecidableEq B]
{G : SynchronousGame X A}
(S : SyncStrategy G)
(H : SynchronousGame X B)
(f : X → A → B)
(hμ : ∀ (x y : X), H.μ x y = G.μ x y)
(hS : S.IsPCC)
:
(S.mergeAnswersByQuestion H f).IsPCC
theorem
MIPRE.SyncStrategy.perfect_mergeAnswersByQuestion
{X : Type u_1}
{A : Type u_2}
{B : Type u_3}
[Fintype X]
[Fintype A]
[DecidableEq A]
[Fintype B]
[DecidableEq B]
{G : SynchronousGame X A}
(S : SyncStrategy G)
(H : SynchronousGame X B)
(f : X → A → B)
(hμ : ∀ (x y : X), H.μ x y = G.μ x y)
(hD :
∀ (x y : X) (a b : A),
0 < G.μ x y → S.P.M x a ≠ 0 → S.P.M y b ≠ 0 → G.D x y a b = true → H.D x y (f x a) (f y b) = true)
(hv : S.value = 1)
:
Perfect play survives any encoder that preserves accepted supported pairs.