Exchanging players in the actual parsed introspection game #
The Pauli predicate is transposed explicitly; no symmetry of that predicate is assumed. The directed auxiliary checks already include both orientations, so the original decision predicate and role-indexed CL maps stay unchanged.
Stated in a bipartite model (Phase 4 of planning/mipco-track.md): exchanging the players is the
swapped model Ξ.swap, whose register model is the swapped register model
(BipartiteModel.regSwap, with both homomorphisms the identity), so the value, the primitive Z
errors and the hiding errors move between the two players with no loss.
def
MIPRE.Introspection.TypedPresentation.edgeSwap
{PauliType : Type u_1}
[Fintype PauliType]
[DecidableEq PauliType]
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(ℓ : ℕ)
:
The exact involution of the uniformly sampled ordered type edges.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPRE.Introspection.TypedPresentation.mu_swap
{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 D' :
CL.Detyping.Question (QuestionType PauliType ℓ) κ → CL.Detyping.Question (QuestionType PauliType ℓ) κ → A → B → Bool)
(x y : CL.Detyping.Question (QuestionType PauliType ℓ) κ)
:
Reversing the ordered edge and retaining the common seed exchanges the two questions, for arbitrary Pauli samplers.
def
MIPRE.Introspection.TypedEstimates.transposePauliPredicate
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{κ : Type u_5}
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
(p q : PauliType)
(x y : κ → ZMod 2)
(a b : PauliAnswer)
:
Transpose every Pauli input, including the actual question contents.
Equations
- MIPRE.Introspection.TypedEstimates.transposePauliPredicate DP p q x y a b = DP q p y x b a
Instances For
theorem
MIPRE.Introspection.TypedEstimates.transposePauliPredicate_transpose
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{κ : Type u_5}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Fintype κ]
[DecidableEq κ]
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
:
theorem
MIPRE.Introspection.TypedEstimates.questionCheck_transpose
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ℓ : ℕ}
(L : Bool → CL.CLFun F ι ℓ)
(X Z : PauliType)
(projectPauli : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
(q r : CL.Detyping.Question (QuestionType PauliType ℓ) κ)
(a b : ParsedAnswer (ι → F) A PauliAnswer)
:
questionCheck L X Z projectPauli D (transposePauliPredicate DP) q r a b = questionCheck L X Z projectPauli D DP r q b a
theorem
MIPRE.Introspection.TypedEstimates.parsedGame_transpose
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ℓ : ℕ}
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(P : PauliType → CL.CLFun (ZMod 2) κ 3)
(L : Bool → CL.CLFun F ι ℓ)
(projectPauli : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
:
parsedGame E X Z P L projectPauli D (transposePauliPredicate DP) = (parsedGame E X Z P L projectPauli D DP).swap
Transposing the Pauli predicate exchanges the players of the parsed game.
theorem
MIPRE.Introspection.TypedEstimates.swap_reg_bornProb
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
{I : Type u_10}
[Fintype I]
[DecidableEq I]
(Y : Matrix I I ℬ)
(X : Matrix I I 𝒜)
:
The register model of the swapped model is the swapped register model: Born probabilities
agree, along regSwap.
theorem
MIPRE.Introspection.TypedEstimates.swap_reg_povmValue
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
{I : Type u_10}
[Fintype I]
[DecidableEq I]
{X' : Type u_11}
{Y' : Type u_12}
{A' : Type u_13}
{B' : Type u_14}
[Fintype X']
[Fintype Y']
[Fintype A']
[Fintype B']
(G : Game X' Y' A' B')
(PA : X' → POVMIn A' (Matrix I I ℬ))
(PB : Y' → POVMIn B' (Matrix I I 𝒜))
:
theorem
MIPRE.Introspection.TypedEstimates.swap_reg_stateSqNorm
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
{I : Type u_10}
[Fintype I]
[DecidableEq I]
(Y : Matrix I I ℬ)
:
theorem
MIPRE.Introspection.TypedEstimates.swap_reg_swap_stateSqNorm
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
{I : Type u_10}
[Fintype I]
[DecidableEq I]
(X : Matrix I I 𝒜)
:
theorem
MIPRE.Introspection.TypedEstimates.swap_reg_xSqNorm
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
{I : Type u_10}
[Fintype I]
[DecidableEq I]
(Y : Matrix I I ℬ)
(X : Matrix I I 𝒜)
:
theorem
MIPRE.Introspection.TypedEstimates.parsedGame_value_swap
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(P : PauliType → CL.CLFun (ZMod 2) κ 3)
(L : Bool → CL.CLFun F ι ℓ)
(projectPauli : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
(MA :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜))
(MB :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ))
:
(Ξ.swap.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D (transposePauliPredicate DP)) MB MA = (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB
The original game's value is preserved by exchanging players and transposing only the supplied Pauli predicate.
theorem
MIPRE.Introspection.TypedEstimates.introBobZError_swap
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(projectPauli : PauliAnswer → ι → F)
(Z : PauliType)
(q : κ → ZMod 2)
(MA :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜))
:
theorem
MIPRE.Introspection.TypedEstimates.introAliceZError_swap
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(projectPauli : PauliAnswer → ι → F)
(Z : PauliType)
(q : κ → ZMod 2)
(MB :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ))
:
theorem
MIPRE.Introspection.TypedEstimates.hidingAliceError_swap
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(L : Bool → CL.CLFun F ι ℓ)
(w : Bool)
(hL : (L w).SupportedOn Finset.univ)
(MB :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ))
(j : Fin ℓ)
:
theorem
MIPRE.Introspection.TypedEstimates.hidingBobError_swap
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(L : Bool → CL.CLFun F ι ℓ)
(w : Bool)
(hL : (L w).SupportedOn Finset.univ)
(MA :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜))
(j : Fin ℓ)
: