Perfect PCC completeness of the full auxiliary introspection game

The game uses every auxiliary type and the exact induced type graph and parsed predicate of introspection. Its honest strategy is explicitly constructed on the seed register tensored with the original strategy. Pauli vertices are not part of this induced game, and no Pauli-completeness assumption is made.

@[reducible, inline]

abbrev MIPRE.Introspection.Honest.AuxEdge {P : Type u_5} [DecidableEq P] {ℓ : ℕ} (E : P → P → Bool) (X Z : P) : Type

The ordered auxiliary edges of the actual introspection graph.

Equations

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

instance MIPRE.Introspection.Honest.auxEdge_nonempty {P : Type u_5} [DecidableEq P] {ℓ : ℕ} (E : P → P → Bool) (X Z : P) : Nonempty (AuxEdge E X Z)

noncomputable def MIPRE.Introspection.Honest.auxGame {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (E : P → P → Bool) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) : Game (AuxQuestion ℓ) (AuxQuestion ℓ) (ParsedAnswer (ι → F) A PA) (ParsedAnswer (ι → F) A PA)

The full induced auxiliary game, retaining all parsed answer constructors.

Equations

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

theorem MIPRE.Introspection.Honest.auxGame_mu_nonadj {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (E : P → P → Bool) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (t u : AuxQuestion ℓ) (hn : ¬TypeGraph.Adj E X Z (Sum.inr t) (Sum.inr u)) : (auxGame L D E X Z projectPauli DP).μ t u = 0

theorem MIPRE.Introspection.Honest.auxGame_mu_pos_adj {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (E : P → P → Bool) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (t u : AuxQuestion ℓ) (h : 0 < (auxGame L D E X Z projectPauli DP).μ t u) : TypeGraph.Adj E X Z (Sum.inr t) (Sum.inr u)

noncomputable def MIPRE.Introspection.Honest.auxStrategy {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (E : P → P → Bool) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) : SyncStrategy (auxGame L D E X Z projectPauli DP).doubled

A single actual synchronous strategy covering all auxiliary types at once.

Equations

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

theorem MIPRE.Introspection.Honest.auxStrategy_dimension {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (E : P → P → Bool) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) : (auxStrategy L D E X Z projectPauli DP R hL).d = Fintype.card (ι → F) * R.d

theorem MIPRE.Introspection.Honest.doubled_adj {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (E : P → P → Bool) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (p q : Bool × AuxQuestion ℓ) (hμ : 0 < (auxGame L D E X Z projectPauli DP).doubled.μ p q) : (p.1 = false ∧ q.1 = true) ∧ TypeGraph.Adj E X Z (Sum.inr p.2) (Sum.inr q.2)

theorem MIPRE.Introspection.Honest.auxStrategy_isPCC {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (E : P → P → Bool) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) : (auxStrategy L D E X Z projectPauli DP R hL).IsPCC

theorem MIPRE.Introspection.Honest.auxStrategy_value {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (E : P → P → Bool) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) (hval : R.value = 1) : (auxStrategy L D E X Z projectPauli DP R hL).value = 1

theorem MIPRE.Introspection.Honest.exists_auxPerfectPCC {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {P : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] [DecidableEq P] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (E : P → P → Bool) (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) (hval : R.value = 1) : ∃ (Q : SyncStrategy (auxGame L D E X Z projectPauli DP).doubled), Q.IsPCC ∧ Q.value = 1 ∧ Q.d = Fintype.card (ι → F) * R.d

Perfect original PCC strategies extend to the full auxiliary introspection game, with exactly the seed-register dimension increase.