Format support of the honest explicit Pauli measurements #
theorem
MIPRE.Introspection.BinaryComplete.strategy_nonzero_pauli_format
{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 : Bool)
(p : QLD.Ty)
(payload : Fin ((3 * m + 3) * t) → ZMod 2)
(a : QLD.Answer F m d)
(ha : (strategy L D R hm b hL).P.M (side, Sum.inl p, payload) (ParsedAnswer.pauli a) ≠ 0)
:
theorem
MIPRE.Introspection.BinaryComplete.quotientHonest_pauli_format
{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 : Bool)
(p : QLD.Ty)
(payload : Fin ((3 * m + 3) * t) → ZMod 2)
(a : QLD.Answer F m d)
(ha : (quotientHonest L D R hm b hL χ π).P.M (side, Sum.inl p, payload) (ParsedAnswer.pauli a) ≠ 0)
: