Perfect PCC completeness of the concrete full typed introspection game

The sampler is the twenty-six-type Pauli CL presentation, with all auxiliary vertices, and the predicate is the actual parsed introspection predicate with the QLD decider. A perfect original PCC strategy gives a perfect PCC strategy on the common seed register tensor the original auxiliary space tensor one qubit. Original CL seeds are indexed by the Pauli field register; no executable compiler or arbitrary seed-padding claim is made here.

@[reducible, inline]

abbrev MIPRE.Introspection.Complete.Question (m t ℓ : ℕ) : Type

Equations

• MIPRE.Introspection.Complete.Question m t ℓ = MIPRE.CL.Detyping.Question (MIPRE.Introspection.QuestionType MIPRE.QLD.Ty ℓ) (Fin ((3 * m + 3) * t))

noncomputable def MIPRE.Introspection.Complete.pauliCheck {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d t : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (p q : QLD.Ty) (x y : Fin ((3 * m + 3) * t) → ZMod 2) : QLD.Answer F m d → QLD.Answer F m d → Bool

Equations

• MIPRE.Introspection.Complete.pauliCheck hm b p q x y = MIPRE.QLD.accepts hm (MIPRE.QLD.PauliCL.binaryQuestion b p x) (MIPRE.QLD.PauliCL.binaryQuestion b q y)

noncomputable def MIPRE.Introspection.Complete.game {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] {m d ℓ t : ℕ} [NeZero m] (L : Bool → CL.CLFun F (Fin m → Bool) ℓ) (D : Seed F m → Seed F m → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) : Game (CL.Detyping.Question (QuestionType QLD.Ty ℓ) (Fin ((3 * m + 3) * t))) (CL.Detyping.Question (QuestionType QLD.Ty ℓ) (Fin ((3 * m + 3) * t))) (ParsedAnswer ((Fin m → Bool) → F) A (QLD.Answer F m d)) (ParsedAnswer ((Fin m → Bool) → F) A (QLD.Answer F m d))

Equations

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

noncomputable def MIPRE.Introspection.Complete.query {F : Type u_1} [Field F] [Fintype F] [Algebra (ZMod 2) F] {m ℓ t : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (p : QuestionType QLD.Ty ℓ) (c : QLD.Content F m) : Question m t ℓ

Equations

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

noncomputable def MIPRE.Introspection.Complete.op {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (L : Bool → CL.CLFun F (Fin m → Bool) ℓ) (D : Seed F m → Seed F m → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (q : Question m t ℓ) : Answer F A m d → Matrix (Space L D R) (Space L D R) ℂ

Equations

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

theorem MIPRE.Introspection.Complete.op_isPVM {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (L : Bool → CL.CLFun F (Fin m → Bool) ℓ) (D : Seed F m → Seed F m → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (q : Question m t ℓ) : IsPVM (op L D R hm b hL q)

theorem MIPRE.Introspection.Complete.op_query {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (L : Bool → CL.CLFun F (Fin m → Bool) ℓ) (D : Seed F m → Seed F m → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (p : QuestionType QLD.Ty ℓ) (c : QLD.Content F m) (a : Answer F A m d) : op L D R hm b hL (query hm b p c) a = sampleOp L D R hm hL c p a

theorem MIPRE.Introspection.Complete.check_query {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (L : Bool → CL.CLFun F (Fin m → Bool) ℓ) (D : Seed F m → Seed F m → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (p q : QuestionType QLD.Ty ℓ) (c : QLD.Content F m) (a a' : Answer F A m d) : (game L D hm b).D (query hm b p c) (query hm b q c) a a' = sampleCheck L D hm c p q a a'

theorem MIPRE.Introspection.Complete.game_positive_content {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (L : Bool → CL.CLFun F (Fin m → Bool) ℓ) (D : Seed F m → Seed F m → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (q r : Question m t ℓ) (h : 0 < (game L D hm b).μ q r) : ∃ (c : QLD.Content F m) (p : QuestionType QLD.Ty ℓ) (s : QuestionType QLD.Ty ℓ), TypeGraph.Adj QLD.adj (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) p s ∧ q = query hm b p c ∧ r = query hm b s c

A positive-probability question pair retains an actual common content witness and an edge of the full introspection graph.

theorem MIPRE.Introspection.Complete.op_commute {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (L : Bool → CL.CLFun F (Fin m → Bool) ℓ) (D : Seed F m → Seed F m → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) (q r : Question m t ℓ) (h : 0 < (game L D hm b).μ q r) (a a' : Answer F A m d) : Commute (op L D R hm b hL q a) (op L D R hm b hL r a')

theorem MIPRE.Introspection.Complete.op_reject {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (L : Bool → CL.CLFun F (Fin m → Bool) ℓ) (D : Seed F m → Seed F m → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (hd : 1 ≤ d) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) (hv : R.value = 1) (q r : Question m t ℓ) (h : 0 < (game L D hm b).μ q r) (a a' : Answer F A m d) (hr : (game L D hm b).D q r a a' = false) : op L D R hm b hL q a * op L D R hm b hL r a' = 0

noncomputable def MIPRE.Introspection.Complete.strategy {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (L : Bool → CL.CLFun F (Fin m → Bool) ℓ) (D : Seed F m → Seed F m → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) : SyncStrategy (game L D hm b).doubled

The actual common-carrier strategy for the complete typed game.

Equations

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

theorem MIPRE.Introspection.Complete.doubled_positive {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (L : Bool → CL.CLFun F (Fin m → Bool) ℓ) (D : Seed F m → Seed F m → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (p q : Bool × Question m t ℓ) (h : 0 < (game L D hm b).doubled.μ p q) : (p.1 = false ∧ q.1 = true) ∧ 0 < (game L D hm b).μ p.2 q.2

theorem MIPRE.Introspection.Complete.strategy_isPCC {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (L : Bool → CL.CLFun F (Fin m → Bool) ℓ) (D : Seed F m → Seed F m → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) : (strategy L D R hm b hL).IsPCC

theorem MIPRE.Introspection.Complete.strategy_value {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (L : Bool → CL.CLFun F (Fin m → Bool) ℓ) (D : Seed F m → Seed F m → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (hd : 1 ≤ d) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) (hv : R.value = 1) : (strategy L D R hm b hL).value = 1

theorem MIPRE.Introspection.Complete.exists_perfectPCC {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t : ℕ} [NeZero m] (L : Bool → CL.CLFun F (Fin m → Bool) ℓ) (D : Seed F m → Seed F m → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (hd : 1 ≤ d) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) (hv : R.value = 1) : ∃ (Q : SyncStrategy (game L D hm b).doubled), Q.IsPCC ∧ Q.value = 1 ∧ Q.d = 2 * Fintype.card (Seed F m) * R.d

Full typed-game completeness with explicit register and source dimension.