Honest binary completeness with the supports required by executable guards

theorem MIPRE.Introspection.BinaryComplete.strategy_nonzero_prefixGuard {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m t d ℓ : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → 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 : Bool × Question m t ℓ) (a : Answer F A m t d) (ha : (strategy L D R hm b hL).P.M q a ≠ 0) : PrefixGuard.holds L q.2.1 a

theorem MIPRE.Introspection.BinaryComplete.strategy_nonzero_introspect {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m t d ℓ : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → 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) (side w : Bool) (payload : Fin ((3 * m + 3) * t) → ZMod 2) (y : Seed m t) (a : A) (ha : (strategy L D R hm b hL).P.M (side, Sum.inr (AuxType.introspect, w), payload) (ParsedAnswer.pair y a) ≠ 0) : ∃ (x : Coord m t → ZMod 2), (L w).eval x = y

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.BinaryComplete.explicitHonest {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m t d ℓ : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → 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) (χ : F → Fin m) (π : F ≃ F) : SyncStrategy (ExplicitGame.game hm χ π b L (project b) D).doubled

Equations

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

theorem MIPRE.Introspection.BinaryComplete.explicitHonest_prefixGuard {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m t d ℓ : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → 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) (χ : F → Fin m) (π : F ≃ F) (q : Bool × Question m t ℓ) (a : Answer F A m t d) (ha : (explicitHonest L D R hm b hL χ π).P.M q a ≠ 0) : PrefixGuard.holds L q.2.1 a

theorem MIPRE.Introspection.BinaryComplete.explicitHonest_introspect {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m t d ℓ : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → 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) (χ : F → Fin m) (π : F ≃ F) (side w : Bool) (payload : Fin ((3 * m + 3) * t) → ZMod 2) (y : Seed m t) (a : A) (ha : (explicitHonest L D R hm b hL χ π).P.M (side, Sum.inr (AuxType.introspect, w), payload) (ParsedAnswer.pair y a) ≠ 0) : ∃ (x : Coord m t → ZMod 2), (L w).eval x = y

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.BinaryComplete.explicitQuotientGame {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] {m t d ℓ : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ 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 (Coord m t → ZMod 2) A (QLD.Answer F m d)) (ParsedAnswer (Coord m t → ZMod 2) A (QLD.Answer F m d))

Equations

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

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.BinaryComplete.quotientHonest {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m t d ℓ : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → 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) (χ : F → Fin m) (π : F ≃ F) : SyncStrategy (explicitQuotientGame L D hm b χ π).doubled

Equations

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

theorem MIPRE.Introspection.BinaryComplete.quotientHonest_prefixGuard {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m t d ℓ : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → 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) (χ : F → Fin m) (π : F ≃ F) (q : Bool × Question m t ℓ) (a : Answer F A m t d) (ha : (quotientHonest L D R hm b hL χ π).P.M q a ≠ 0) : PrefixGuard.holds L q.2.1 a

theorem MIPRE.Introspection.BinaryComplete.quotientHonest_introspect {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m t d ℓ : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → 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) (χ : F → Fin m) (π : F ≃ F) (side w : Bool) (payload : Fin ((3 * m + 3) * t) → ZMod 2) (y : Seed m t) (a : A) (ha : (quotientHonest L D R hm b hL χ π).P.M (side, Sum.inr (AuxType.introspect, w), payload) (ParsedAnswer.pair y a) ≠ 0) : ∃ (x : Coord m t → ZMod 2), (L w).eval x = y

theorem MIPRE.Introspection.BinaryComplete.quotientHonest_isPCC {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m t d ℓ : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → 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) (χ : F → Fin m) (π : F ≃ F) (hb : LowDegree.IsSelfDualBasis b) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) (hR : R.IsPCC) : (quotientHonest L D R hm b hL χ π).IsPCC

theorem MIPRE.Introspection.BinaryComplete.quotientHonest_value {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m t d ℓ : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → 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) (χ : F → Fin m) (π : F ≃ F) (hb : LowDegree.IsSelfDualBasis b) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) (hd : 1 ≤ d) (hR : R.IsPCC) (hv : R.value = 1) : (quotientHonest L D R hm b hL χ π).value = 1

theorem MIPRE.Introspection.BinaryComplete.quotientHonest_dimension {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m t d ℓ : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Coord m t) ℓ) (D : Seed m t → Seed m t → 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) (χ : F → Fin m) (π : F ≃ F) : (quotientHonest L D R hm b hL χ π).d = 2 * Fintype.card (Seed m t) * R.d