Documentation

MIPRE.Foundations.Introspection.PrefixGuardGame

Adding honest prefix guards preserves completeness #

Changing a predicate only on zero measurement effects preserves its value. Applying this observation to the local prefix guards keeps the honest state, dimension and PCC property, while guard rejection can only reduce arbitrary strategies' success.

source
theorem MIPRE.SyncStrategy.value_copy_of_nonzero {X : Type u_1} {A : Type u_2} [Fintype X] [Fintype A] [DecidableEq A] {G : SynchronousGame X A} (S : SyncStrategy G) (G' : SynchronousGame X A) (hμ : ∀ (x y : X), G'.μ x y = G.μ x y) (hD : ∀ (x y : X) (a b : A), S.P.M x a ≠ 0 → S.P.M y b ≠ 0 → G'.D x y a b = G.D x y a b) :
(S.copy G').value = S.value

Predicate agreement is needed only on nonzero measurement effects.

source
noncomputable def MIPRE.Introspection.PrefixGuard.game {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} {Q : Type u_6} [Field F] [Fintype F] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype PA] [Fintype Q] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (type : Q → QuestionType P ℓ) (G : Game Q Q (ParsedAnswer (ι → F) A PA) (ParsedAnswer (ι → F) A PA)) :
Game Q Q (ParsedAnswer (ι → F) A PA) (ParsedAnswer (ι → F) A PA)

Retain the question law and add both local prefix checks. Raw question payloads remain available to the original predicate.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem MIPRE.Introspection.PrefixGuard.game_mu {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} {Q : Type u_6} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq PA] [Fintype Q] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (type : Q → QuestionType P ℓ) (G : Game Q Q (ParsedAnswer (ι → F) A PA) (ParsedAnswer (ι → F) A PA)) (q r : Q) :
    (game L type G).μ q r = G.μ q r
    source
    theorem MIPRE.Introspection.PrefixGuard.game_accepts_iff {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} {Q : Type u_6} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq PA] [Fintype Q] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (type : Q → QuestionType P ℓ) (G : Game Q Q (ParsedAnswer (ι → F) A PA) (ParsedAnswer (ι → F) A PA)) (q r : Q) (a b : ParsedAnswer (ι → F) A PA) :
    (game L type G).D q r a b = true ↔ holds L (type q) a ∧ holds L (type r) b ∧ G.D q r a b = true
    source
    theorem MIPRE.Introspection.PrefixGuard.copied_value {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} {Q : Type u_6} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq PA] [Fintype Q] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (type : Q → QuestionType P ℓ) (G : Game Q Q (ParsedAnswer (ι → F) A PA) (ParsedAnswer (ι → F) A PA)) (S : SyncStrategy G.doubled) (hS : ∀ (q : Bool × Q) (a : ParsedAnswer (ι → F) A PA), S.P.M q a ≠ 0 → holds L (type q.2) a) :
    (S.copy (game L type G).doubled).value = S.value

    Any strategy whose nonzero effects satisfy the guard retains its exact value, without requiring perfection as an intermediate premise.

    source
    theorem MIPRE.Introspection.PrefixGuard.copied_value_eq_one {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} {Q : Type u_6} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq PA] [Fintype Q] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (type : Q → QuestionType P ℓ) (G : Game Q Q (ParsedAnswer (ι → F) A PA) (ParsedAnswer (ι → F) A PA)) (S : SyncStrategy G.doubled) (hS : ∀ (q : Bool × Q) (a : ParsedAnswer (ι → F) A PA), S.P.M q a ≠ 0 → holds L (type q.2) a) (hv : S.value = 1) :
    (S.copy (game L type G).doubled).value = 1
    source
    theorem MIPRE.Introspection.PrefixGuard.copied_isPCC {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} {Q : Type u_6} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq PA] [Fintype Q] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (type : Q → QuestionType P ℓ) (G : Game Q Q (ParsedAnswer (ι → F) A PA) (ParsedAnswer (ι → F) A PA)) (S : SyncStrategy G.doubled) (hS : S.IsPCC) :
    (S.copy (game L type G).doubled).IsPCC
    source
    @[simp]
    theorem MIPRE.Introspection.PrefixGuard.copied_dimension {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} {Q : Type u_6} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq PA] [Fintype Q] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (type : Q → QuestionType P ℓ) (G : Game Q Q (ParsedAnswer (ι → F) A PA) (ParsedAnswer (ι → F) A PA)) (S : SyncStrategy G.doubled) :
    (S.copy (game L type G).doubled).d = S.d