The errors at unchanged questions survive adaptive replacement exactly #
The replacement at the selected question is arbitrary. Every other question is the concrete identity extension in the original register ordering. Consequently the primitive Pauli estimates and the hiding and Read estimates can be reused at the next induction stage without an additional error.
Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the old register state is the
register model Ξ.reg I, the new one the register model (Ξ.expandA t₀).reg I of the auxiliary
model extended by a first-player ancilla in the fixed state t₀. At an unchanged question the
registered replacement is the old measurement carried along the registered extension
registeredExtend Ξ t₀ (registeredExtendPOVM), a local isometry taking the state to the state,
so every error is transported exactly. An honest register operator enters as smulKron 1 J and
is fixed by the extension (registeredExtendOp_aOp); the second player's operators are unchanged.
theorem
MIPRE.Introspection.registeredReplacement_other_eq
{𝒜 : Type u_2}
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
{X : Type u_4}
{I : Type u_5}
{T : Type u_6}
{A : Type u_7}
[Fintype X]
[DecidableEq X]
[Fintype I]
[DecidableEq I]
[Fintype T]
[DecidableEq T]
[Fintype A]
(MA : X → POVMIn A (Matrix I I 𝒜))
(q x : X)
(R : POVMIn A (Matrix T T (Matrix I I 𝒜)))
(hx : x ≠ q)
:
theorem
MIPRE.Introspection.registeredReplacement_other_map
{𝒜 : Type u_2}
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
{X : Type u_4}
{I : Type u_5}
{T : Type u_6}
{A : Type u_7}
{B : Type u_8}
[Fintype X]
[DecidableEq X]
[Fintype I]
[DecidableEq I]
[Fintype T]
[DecidableEq T]
[Fintype A]
[Fintype B]
[DecidableEq B]
(MA : X → POVMIn A (Matrix I I 𝒜))
(q x : X)
(R : POVMIn A (Matrix T T (Matrix I I 𝒜)))
(hx : x ≠ q)
(f : A → B)
:
Outcome maps, including their malformed outcome, are transported exactly.
theorem
MIPRE.Introspection.registeredReplacement_samePartyError_other
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ 𝒜]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
{X : Type u_4}
{I : Type u_5}
{T : Type u_6}
{A : Type u_7}
{B : Type u_8}
[Fintype X]
[DecidableEq X]
[Fintype I]
[DecidableEq I]
[Fintype T]
[DecidableEq T]
[Fintype A]
[Fintype B]
[DecidableEq B]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(t₀ : T)
(MA : X → POVMIn A (Matrix I I 𝒜))
(q x : X)
(R : POVMIn A (Matrix T T (Matrix I I 𝒜)))
(hx : x ≠ q)
(f : A → B)
(J : B → Matrix I I ℂ)
:
∑ b : B, ((Ξ.expandA t₀).reg I).stateSqNorm ((POVMIn.map f (registeredReplacement MA q R x)).op b - smulKron 1 (J b)) = ∑ b : B, (Ξ.reg I).stateSqNorm ((POVMIn.map f (MA x)).op b - smulKron 1 (J b))
theorem
MIPRE.Introspection.registeredReplacement_crossError_other
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ 𝒜]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
{X : Type u_4}
{I : Type u_5}
{T : Type u_6}
{A : Type u_7}
{B : Type u_8}
[Fintype X]
[DecidableEq X]
[Fintype I]
[DecidableEq I]
[Fintype T]
[DecidableEq T]
[Fintype A]
[Fintype B]
[DecidableEq B]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(t₀ : T)
(MA : X → POVMIn A (Matrix I I 𝒜))
(q x : X)
(R : POVMIn A (Matrix T T (Matrix I I 𝒜)))
(hx : x ≠ q)
(f : A → B)
(N : B → Matrix I I ℬ)
:
∑ b : B, ((Ξ.expandA t₀).reg I).xSqNorm ((POVMIn.map f (registeredReplacement MA q R x)).op b) (N b) = ∑ b : B, (Ξ.reg I).xSqNorm ((POVMIn.map f (MA x)).op b) (N b)
theorem
MIPRE.Introspection.registeredExtension_bobCrossError
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
{I : Type u_5}
{T : Type u_6}
{B : Type u_8}
[Fintype I]
[DecidableEq I]
[Fintype T]
[DecidableEq T]
[Fintype B]
[DecidableEq B]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(t₀ : T)
(J : B → Matrix I I ℂ)
(N : B → Matrix I I ℬ)
:
theorem
MIPRE.Introspection.registeredExtension_bobSamePartyError
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
{I : Type u_5}
{T : Type u_6}
{B : Type u_8}
[Fintype I]
[DecidableEq I]
[Fintype T]
[DecidableEq T]
[Fintype B]
[DecidableEq B]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(t₀ : T)
(N : B → Matrix I I ℬ)
:
The first player's errors at the unchanged questions #
theorem
MIPRE.Introspection.TypedEstimates.hidingAliceError_registeredReplacement
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
{T : Type u_7}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
[Fintype T]
[DecidableEq T]
{ℓ : ℕ}
{𝒞 : Type u_8}
{𝒜 : Type u_9}
{ℬ : Type u_10}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ 𝒜]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
(L : Bool → CL.CLFun F ι ℓ)
(w v : Bool)
(hL : (L w).SupportedOn Finset.univ)
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(t₀ : T)
(MA :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜))
(R : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix T T (Matrix (ι → F) (ι → F) 𝒜)))
(j : Fin ℓ)
:
hidingAliceError L w hL (Ξ.expandA t₀) (registeredReplacement MA (QuestionType.introspect v, 0) R) j = hidingAliceError L w hL Ξ MA j
theorem
MIPRE.Introspection.TypedEstimates.readAliceError_registeredReplacement
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
{T : Type u_7}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
[Fintype T]
[DecidableEq T]
{ℓ : ℕ}
{𝒞 : Type u_8}
{𝒜 : Type u_9}
{ℬ : Type u_10}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ 𝒜]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
(L : Bool → CL.CLFun F ι ℓ)
(w v : Bool)
(hL : (L w).SupportedOn Finset.univ)
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(t₀ : T)
(MA :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜))
(R : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix T T (Matrix (ι → F) (ι → F) 𝒜)))
(j : Fin ℓ)
:
readAliceError L w hL (Ξ.expandA t₀) (registeredReplacement MA (QuestionType.introspect v, 0) R) j = readAliceError L w hL Ξ MA j
theorem
MIPRE.Introspection.TypedEstimates.pauliAliceError_registeredReplacement
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
{T : Type u_7}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
[Fintype T]
[DecidableEq T]
{ℓ : ℕ}
{𝒞 : Type u_8}
{𝒜 : Type u_9}
{ℬ : Type u_10}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ 𝒜]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(t₀ : T)
(projectPauli : PauliAnswer → ι → F)
(MA :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜))
(R : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix T T (Matrix (ι → F) (ι → F) 𝒜)))
(v : Bool)
(p : PauliType)
(q : κ → ZMod 2)
(J : Option (ι → F) → Matrix (ι → F) (ι → F) ℂ)
:
∑ z : Option (ι → F),
((Ξ.expandA t₀).reg (ι → F)).stateSqNorm
((POVMIn.map (pauliProjection projectPauli)
(registeredReplacement MA (QuestionType.introspect v, 0) R (QuestionType.pauli p, q))).op
z - smulKron 1 (J z)) = ∑ z : Option (ι → F),
(Ξ.reg (ι → F)).stateSqNorm
((POVMIn.map (pauliProjection projectPauli) (MA (QuestionType.pauli p, q))).op z - smulKron 1 (J z))
The primitive Alice Pauli estimate, for any fixed register ideal, is unchanged when an Introspect question is replaced.
The second player's errors on the extended state #
theorem
MIPRE.Introspection.TypedEstimates.hidingBobError_registeredExtension
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
{T : Type u_7}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
[Fintype T]
[DecidableEq T]
{ℓ : ℕ}
{𝒞 : Type u_8}
{𝒜 : Type u_9}
{ℬ : Type u_10}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(L : Bool → CL.CLFun F ι ℓ)
(w : Bool)
(hL : (L w).SupportedOn Finset.univ)
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(t₀ : T)
(MB :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ))
(j : Fin ℓ)
:
theorem
MIPRE.Introspection.TypedEstimates.readBobError_registeredExtension
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
{T : Type u_7}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
[Fintype T]
[DecidableEq T]
{ℓ : ℕ}
{𝒞 : Type u_8}
{𝒜 : Type u_9}
{ℬ : Type u_10}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(L : Bool → CL.CLFun F ι ℓ)
(w : Bool)
(hL : (L w).SupportedOn Finset.univ)
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(t₀ : T)
(MB :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ))
(j : Fin ℓ)
:
theorem
MIPRE.Introspection.TypedEstimates.pauliBobError_registeredExtension
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
{T : Type u_7}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
[Fintype T]
[DecidableEq T]
{ℓ : ℕ}
{𝒞 : Type u_8}
{𝒜 : Type u_9}
{ℬ : Type u_10}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(t₀ : T)
(projectPauli : PauliAnswer → ι → F)
(MB :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ))
(p : PauliType)
(q : κ → ZMod 2)
(J : Option (ι → F) → Matrix (ι → F) (ι → F) ℂ)
:
∑ z : Option (ι → F),
((Ξ.expandA t₀).reg (ι → F)).snorm
(((Ξ.expandA t₀).reg (ι → F)).πB
((POVMIn.map (pauliProjection projectPauli) (MB (QuestionType.pauli p, q))).op z - smulKron 1 (J z))) ^ 2 = ∑ z : Option (ι → F),
(Ξ.reg (ι → F)).snorm
((Ξ.reg (ι → F)).πB
((POVMIn.map (pauliProjection projectPauli) (MB (QuestionType.pauli p, q))).op z - smulKron 1 (J z))) ^ 2
The primitive Bob Pauli estimate is unchanged on the newly extended state; Bob's actual family is literally retained.