Actual Pauli/auxiliary edge probabilities and agreement estimates

The Pauli-X and Pauli-Z vertices have a fixed question. We state that property explicitly: the generic Pauli CL family supplied to the typed construction does not itself force their question to be zero. Both edge orientations have exactly inverse ordered-edge-count probability.

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

theorem MIPRE.Introspection.TypedPresentation.mu_constant_edge {PauliType : Type u_1} {κ : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Fintype A] [Fintype B] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (D : CL.Detyping.Question (QuestionType PauliType ℓ) κ → CL.Detyping.Question (QuestionType PauliType ℓ) κ → A → B → Bool) (t u : QuestionType PauliType ℓ) (x y : κ → ZMod 2) (ht : ∀ (z : κ → ZMod 2), (family P t).eval z = x) (hu : ∀ (z : κ → ZMod 2), (family P u).eval z = y) (hedge : TypeGraph.Adj E X Z t u) : (game E X Z ℓ P D).μ (t, x) (u, y) = (↑(TypeGraph.edges E X Z ℓ).card)⁻¹

An edge whose two questions are constant has exactly its ordered-edge probability; no injectivity of the sampler's seed map is needed.

theorem MIPRE.Introspection.TypedPresentation.mu_pauli_aux {PauliType : Type u_1} {κ : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Fintype A] [Fintype B] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (D : CL.Detyping.Question (QuestionType PauliType ℓ) κ → CL.Detyping.Question (QuestionType PauliType ℓ) κ → A → B → Bool) (p : PauliType) (q : κ → ZMod 2) (hq : ∀ (z : κ → ZMod 2), (P p).eval z = q) (t : AuxType ℓ) (w : Bool) (hedge : TypeGraph.Adj E X Z (Sum.inl p) (Sum.inr (t, w))) : (game E X Z ℓ P D).μ (Sum.inl p, q) (Sum.inr (t, w), 0) = (↑(TypeGraph.edges E X Z ℓ).card)⁻¹

theorem MIPRE.Introspection.TypedPresentation.mu_aux_pauli {PauliType : Type u_1} {κ : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Fintype A] [Fintype B] {ℓ : ℕ} (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (D : CL.Detyping.Question (QuestionType PauliType ℓ) κ → CL.Detyping.Question (QuestionType PauliType ℓ) κ → A → B → Bool) (t : AuxType ℓ) (w : Bool) (p : PauliType) (q : κ → ZMod 2) (hq : ∀ (z : κ → ZMod 2), (P p).eval z = q) (hedge : TypeGraph.Adj E X Z (Sum.inr (t, w)) (Sum.inl p)) : (game E X Z ℓ P D).μ (Sum.inr (t, w), 0) (Sum.inl p, q) = (↑(TypeGraph.edges E X Z ℓ).card)⁻¹

def MIPRE.Introspection.TypedEstimates.pauliProjection {V : Type u_9} {A : Type u_10} {PA : Type u_11} (projectPauli : PA → V) : ParsedAnswer V A PA → Option V

Project the tested Pauli answer, retaining all wrong constructors as a separate malformed outcome.

Equations

• MIPRE.Introspection.TypedEstimates.pauliProjection projectPauli (MIPRE.Introspection.ParsedAnswer.pauli a) = some (projectPauli a)
• MIPRE.Introspection.TypedEstimates.pauliProjection projectPauli x✝ = none

theorem MIPRE.Introspection.TypedEstimates.constant_edge_agreement_estimate {PauliType : Type u_1} {κ : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Fintype A] [Fintype B] [Fintype C] [DecidableEq C] {ℓ : ℕ} {𝒞 : Type u_6} {𝒜 : Type u_7} {ℬ : Type u_8} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (D : CL.Detyping.Question (QuestionType PauliType ℓ) κ → CL.Detyping.Question (QuestionType PauliType ℓ) κ → A → B → Bool) (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (hΨ : ‖Ψ.ψ‖ = 1) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn A 𝒜) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn B ℬ) {ε : ℝ} (hfail : 1 - Ψ.povmValue (TypedPresentation.game E X Z ℓ P D) MA MB ≤ ε) (t u : QuestionType PauliType ℓ) (x y : κ → ZMod 2) (ht : ∀ (z : κ → ZMod 2), (TypedPresentation.family P t).eval z = x) (hu : ∀ (z : κ → ZMod 2), (TypedPresentation.family P u).eval z = y) (hedge : TypeGraph.Adj E X Z t u) (f : A → C) (g : B → C) (hcheck : ∀ (a : A) (b : B), D (t, x) (u, y) a b = true → f a = g b) : ∑ z : C, Ψ.xSqNorm ((POVMIn.map f (MA (t, x))).op z) ((POVMIn.map g (MB (u, y))).op z) ≤ 2 * ↑(TypeGraph.edges E X Z ℓ).card * ε

On an edge whose two questions are constant, the coarsened cross-party distance costs twice the ordered-edge count times the game's failure.

theorem MIPRE.Introspection.TypedEstimates.pauli_aux_agreement_estimate {PauliType : Type u_1} {κ : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Fintype A] [Fintype B] [Fintype C] [DecidableEq C] {ℓ : ℕ} {𝒞 : Type u_6} {𝒜 : Type u_7} {ℬ : Type u_8} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (D : CL.Detyping.Question (QuestionType PauliType ℓ) κ → CL.Detyping.Question (QuestionType PauliType ℓ) κ → A → B → Bool) (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (hΨ : ‖Ψ.ψ‖ = 1) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn A 𝒜) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn B ℬ) {ε : ℝ} (hfail : 1 - Ψ.povmValue (TypedPresentation.game E X Z ℓ P D) MA MB ≤ ε) (p : PauliType) (q : κ → ZMod 2) (hq : ∀ (z : κ → ZMod 2), (P p).eval z = q) (t : AuxType ℓ) (w : Bool) (hedge : TypeGraph.Adj E X Z (Sum.inl p) (Sum.inr (t, w))) (f : A → C) (g : B → C) (hcheck : ∀ (a : A) (b : B), D (Sum.inl p, q) (Sum.inr (t, w), 0) a b = true → f a = g b) : ∑ z : C, Ψ.xSqNorm ((POVMIn.map f (MA (Sum.inl p, q))).op z) ((POVMIn.map g (MB (Sum.inr (t, w), 0))).op z) ≤ 2 * ↑(TypeGraph.edges E X Z ℓ).card * ε

theorem MIPRE.Introspection.TypedEstimates.aux_pauli_agreement_estimate {PauliType : Type u_1} {κ : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Fintype A] [Fintype B] [Fintype C] [DecidableEq C] {ℓ : ℕ} {𝒞 : Type u_6} {𝒜 : Type u_7} {ℬ : Type u_8} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (D : CL.Detyping.Question (QuestionType PauliType ℓ) κ → CL.Detyping.Question (QuestionType PauliType ℓ) κ → A → B → Bool) (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (hΨ : ‖Ψ.ψ‖ = 1) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn A 𝒜) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn B ℬ) {ε : ℝ} (hfail : 1 - Ψ.povmValue (TypedPresentation.game E X Z ℓ P D) MA MB ≤ ε) (t : AuxType ℓ) (w : Bool) (p : PauliType) (q : κ → ZMod 2) (hq : ∀ (z : κ → ZMod 2), (P p).eval z = q) (hedge : TypeGraph.Adj E X Z (Sum.inr (t, w)) (Sum.inl p)) (f : A → C) (g : B → C) (hcheck : ∀ (a : A) (b : B), D (Sum.inr (t, w), 0) (Sum.inl p, q) a b = true → f a = g b) : ∑ z : C, Ψ.xSqNorm ((POVMIn.map f (MA (Sum.inr (t, w), 0))).op z) ((POVMIn.map g (MB (Sum.inl p, q))).op z) ≤ 2 * ↑(TypeGraph.edges E X Z ℓ).card * ε