Restricting a parsed introspection strategy to its Pauli tests

Malformed outer answer constructors are completed at a fixed Pauli answer. Every originally accepted Pauli answer pair remains accepted, including on loops, where the parsed predicate checks both consistency and the Pauli rule. The uniform full type graph bounds the mean failure along each of its edges.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md).

def MIPRE.Introspection.completePauliAnswer {V : Type u_1} {A : Type u_2} {PA : Type u_3} (a₀ : PA) : ParsedAnswer V A PA → PA

Retain an actual Pauli answer and complete every other constructor.

Equations

• MIPRE.Introspection.completePauliAnswer a₀ (MIPRE.Introspection.ParsedAnswer.pauli a) = a
• MIPRE.Introspection.completePauliAnswer a₀ x✝ = a₀

def MIPRE.Introspection.completePauliPOVM {V : Type u_1} {A : Type u_2} {PA : Type u_3} [Fintype V] [Fintype A] [Fintype PA] [DecidableEq PA] {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (a₀ : PA) (M : POVMIn (ParsedAnswer V A PA) R) : POVMIn PA R

The parsed measurement coarse-grained along completePauliAnswer a₀, in any ordered ⋆-ring: either player's algebra.

Equations

• MIPRE.Introspection.completePauliPOVM a₀ M = MIPRE.POVMIn.map (MIPRE.Introspection.completePauliAnswer a₀) M

theorem MIPRE.Introspection.completePauliPOVM_isPVM {V : Type u_1} {A : Type u_2} {PA : Type u_3} [Fintype V] [Fintype A] [Fintype PA] [DecidableEq PA] {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (a₀ : PA) (M : POVMIn (ParsedAnswer V A PA) R) (hM : IsPVMIn M.op) : IsPVMIn (completePauliPOVM a₀ M).op

theorem MIPRE.Introspection.completePauliPOVM_mats {V : Type u_1} {A : Type u_2} {PA : Type u_3} [Fintype V] [Fintype A] [Fintype PA] [DecidableEq PA] {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (a₀ a : PA) (M : POVMIn (ParsedAnswer V A PA) R) : (completePauliPOVM a₀ M).op a = ∑ b : ParsedAnswer V A PA with completePauliAnswer a₀ b = a, M.op b

theorem MIPRE.Introspection.completePauliPOVM_mats_of_ne {V : Type u_1} {A : Type u_2} {PA : Type u_3} [Fintype V] [Fintype A] [Fintype PA] [DecidableEq PA] {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (a₀ a : PA) (ha : a ≠ a₀) (M : POVMIn (ParsedAnswer V A PA) R) : (completePauliPOVM a₀ M).op a = M.op (ParsedAnswer.pauli a)

Only the selected completion answer changes its operator.

theorem MIPRE.Introspection.TypedEstimates.check_pauli_completed {T : Type u_1} {F : Type u_2} {ι : Type u_3} {A : Type u_5} {PA : Type u_6} [Fintype T] [DecidableEq T] [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [Fintype PA] [DecidableEq PA] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z p q : T) (project : PA → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : T → T → PA → PA → Bool) (a₀ b₀ : PA) (a b : ParsedAnswer (ι → F) A PA) (h : TypedPredicate.check L X Z project D DP (Sum.inl p) (Sum.inl q) a b = true) : DP p q (completePauliAnswer a₀ a) (completePauliAnswer b₀ b) = true

theorem MIPRE.Introspection.TypedEstimates.completed_pauli_condFail_le {T : Type u_1} {F : Type u_2} {ι : Type u_3} {κ : Type u_4} {A : Type u_5} {PA : Type u_6} [Fintype T] [DecidableEq T] [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] [Fintype PA] [DecidableEq PA] {ℓ : ℕ} {𝒞 : Type u_7} {𝒜 : Type u_8} {ℬ : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (E : T → T → Bool) (X Z : T) (P : T → CL.CLFun (ZMod 2) κ 3) (L : Bool → CL.CLFun F ι ℓ) (project : PA → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : T → T → (κ → ZMod 2) → (κ → ZMod 2) → PA → PA → Bool) (GP : Game (CL.Detyping.Question T κ) (CL.Detyping.Question T κ) PA PA) (hDP : ∀ (x y : CL.Detyping.Question T κ) (a b : PA), GP.D x y a b = DP x.1 y.1 x.2 y.2 a b) (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (MA : CL.Detyping.Question (QuestionType T ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PA) 𝒜) (MB : CL.Detyping.Question (QuestionType T ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PA) ℬ) (a₀ b₀ : PA) (x y : CL.Detyping.Question T κ) : Ψ.condFail GP (fun (x : CL.Detyping.Question T κ) => completePauliPOVM a₀ (MA (Sum.inl x.1, x.2))) (fun (y : CL.Detyping.Question T κ) => completePauliPOVM b₀ (MB (Sum.inl y.1, y.2))) x y ≤ Ψ.condFail (parsedGame E X Z P L project D DP) MA MB (Sum.inl x.1, x.2) (Sum.inl y.1, y.2)

Completion can only improve the conditional Pauli success probability.

theorem MIPRE.Introspection.TypedEstimates.typed_edge_mean_failure_le {T : Type u_1} {κ : Type u_4} {A : Type u_5} [Fintype T] [DecidableEq T] [Fintype κ] [DecidableEq κ] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_7} {𝒜 : Type u_8} {ℬ : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {B : Type u_10} [Fintype B] (E : T → T → Bool) (X Z : T) (P : T → CL.CLFun (ZMod 2) κ 3) (D : CL.Detyping.Question (QuestionType T ℓ) κ → CL.Detyping.Question (QuestionType T ℓ) κ → A → B → Bool) (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (hΨ : ‖Ψ.ψ‖ = 1) (MA : CL.Detyping.Question (QuestionType T ℓ) κ → POVMIn A 𝒜) (MB : CL.Detyping.Question (QuestionType T ℓ) κ → POVMIn B ℬ) {ε : ℝ} (hf : 1 - Ψ.povmValue (TypedPresentation.game E X Z ℓ P D) MA MB ≤ ε) (p q : QuestionType T ℓ) (hpq : TypeGraph.Adj E X Z p q) : (∑ z : κ → ZMod 2, Ψ.condFail (TypedPresentation.game E X Z ℓ P D) MA MB (p, (TypedPresentation.family P p).eval z) (q, (TypedPresentation.family P q).eval z)) / ↑(Fintype.card (κ → ZMod 2)) ≤ ↑(TypeGraph.edges E X Z ℓ).card * ε

The full uniform type graph bounds the seed-averaged failure on each individual edge, without requiring injectivity of the question maps.