A successor of the actual Introspect induction #
The current game's tests construct the replacement. Canonicalization and decoder recovery discharge the selected-measurement identity, and decoding gives the next structural invariant. The fixed hiding and primitive Z errors can be reused on the enlarged auxiliary space.
Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the register state is the
register model Ξ.reg (ι → F) of a normalized auxiliary model Ξ, and the successor lives on the
register model (Ξ.expandA t₀).reg (ι → F) of its one-sided extension by the dilation ancilla
DilationAncilla (Option ((ι → F) × A)) K in its fixed state t₀ = inl (none, 0). The size K
is chosen by the dilation (exists_game_adaptive_prefix_dilation), so the successor theorem
returns it. The successor family is the registered replacement, a family of POVMs in
Matrix (ι → F) (ι → F) (Matrix T T 𝒜), and its invariant is the decoded next-prefix invariant
over that algebra. The primitive Z errors of both players (introAliceZError, defined here next
to introBobZError) and their hiding errors are transported exactly to the extended model
(StrategyReplacementErrors); the successor theorem records these equalities for the iteration.
noncomputable def
MIPRE.Introspection.introSuccessorFamily
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[Fintype A]
{ℓ : ℕ}
{𝒜 : Type u_8}
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
{T : Type u_10}
[Fintype T]
[DecidableEq T]
(P : CL.CLFun F ι ℓ)
(hP : P.SupportedOn Finset.univ)
(k : ℕ)
(MA :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜))
(w : Bool)
(R : AdaptiveDilationFamily P k 𝒜 T (Option ((ι → F) × A)))
(hR : ∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (R y z))
:
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) (Matrix T T 𝒜))
The actual question-indexed family after inserting the decoded replacement, with the original family retained at every other question.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPRE.Introspection.introSuccessorFamily_isPVM
{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_8}
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
{T : Type u_10}
[Fintype T]
[DecidableEq T]
(P : CL.CLFun F ι ℓ)
(hP : P.SupportedOn Finset.univ)
(k : ℕ)
(MA :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜))
(w : Bool)
(R : AdaptiveDilationFamily P k 𝒜 T (Option ((ι → F) × A)))
(hR : ∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (R y z))
(hMA : ∀ (q : CL.Detyping.Question (QuestionType PauliType ℓ) κ), IsPVMIn (MA q).op)
(q : CL.Detyping.Question (QuestionType PauliType ℓ) κ)
:
IsPVMIn (introSuccessorFamily P hP k MA w R hR q).op
noncomputable def
MIPRE.Introspection.introSuccessorInvariant
{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_8}
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
{T : Type u_10}
[Fintype T]
[DecidableEq T]
(P : CL.CLFun F ι ℓ)
(hP : P.SupportedOn Finset.univ)
(k : ℕ)
(MA :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜))
(w : Bool)
(R : AdaptiveDilationFamily P k 𝒜 T (Option ((ι → F) × A)))
(hR : ∀ (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), IsPVMIn (R y z))
:
IntroPrefixInvariant P (k + 1)
(POVMIn.map TypedEstimates.introspectPair (introSuccessorFamily P hP k MA w R hR (QuestionType.introspect w, 0)))
The returned raw selected measurement carries the complete next option-valued product form, including valid-answer support.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MIPRE.Introspection.TypedEstimates.introBobZError
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[Fintype PauliAnswer]
[Fintype F]
[DecidableEq F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(projectPauli : PauliAnswer → ι → F)
(Z : PauliType)
(q : κ → ZMod 2)
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(MB :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ))
:
The primitive Bob-Z error in the common register model.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPRE.Introspection.TypedEstimates.introBobZError_extVecA
{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 ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
{T : Type u_10}
[Fintype T]
[DecidableEq T]
(projectPauli : PauliAnswer → ι → F)
(Z : PauliType)
(q : κ → ZMod 2)
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(t₀ : T)
(MB :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ))
:
The primitive Bob-Z error is unchanged by a first-player ancilla in a fixed state.
noncomputable def
MIPRE.Introspection.TypedEstimates.introAliceZError
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[Fintype PauliAnswer]
[Fintype F]
[DecidableEq F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
(projectPauli : PauliAnswer → ι → F)
(Z : PauliType)
(q : κ → ZMod 2)
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(MA :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜))
:
Alice's primitive computational-basis error, with malformed Pauli answers kept as the separate option outcome.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPRE.Introspection.TypedEstimates.exists_intro_successor
{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 ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ 𝒜]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
[StarModule ℂ ℬ]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(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)
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(hΞ : ‖Ξ.ψ‖ = 1)
(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) ℬ))
(hMA : ∀ (q : CL.Detyping.Question (QuestionType PauliType ℓ) κ), IsPVMIn (MA q).op)
(hMB : ∀ (q : CL.Detyping.Question (QuestionType PauliType ℓ) κ), IsPVMIn (MB q).op)
(q : κ → ZMod 2)
(hq : ∀ (z : κ → ZMod 2), (P Z).eval z = q)
(w : Bool)
(hL : (L w).SupportedOn Finset.univ)
(j : Fin ℓ)
(I : IntroPrefixInvariant (L w) (↑j) (POVMIn.map introspectPair (MA (QuestionType.introspect w, 0))))
{ε η δ : ℝ}
(hε : 0 ≤ ε)
(hη : 0 ≤ η)
(hδ : 0 ≤ δ)
(hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε)
(hZ : introBobZError projectPauli Z q Ξ MB ≤ η)
(hhide : hidingAliceError L w hL Ξ MA j ≤ δ)
(hsmall : adaptiveStageBudget (ℓ - ↑j) (↑(TypeGraph.edges E X Z ℓ).card * ε) η δ ≤ 1)
:
∃ (K : ℕ) (MA' :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer)
(Matrix (ι → F) (ι → F)
(Matrix (DilationAncilla (Option ((ι → F) × A)) K) (DilationAncilla (Option ((ι → F) × A)) K) 𝒜)))
(x : IntroPrefixInvariant (L w) (↑j + 1) (POVMIn.map introspectPair (MA' (QuestionType.introspect w, 0)))),
(∀ (t : CL.Detyping.Question (QuestionType PauliType ℓ) κ), IsPVMIn (MA' t).op) ∧ 1 - ((Ξ.expandA (Sum.inl (none, 0))).reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA' MB ≤ ε + adaptiveStepLoss (adaptiveStageBudget (ℓ - ↑j) (↑(TypeGraph.edges E X Z ℓ).card * ε) η δ) ∧ (∀ (t : QuestionType PauliType ℓ × (κ → ZMod 2)),
t ≠ (QuestionType.introspect w, 0) → MA' t = registeredExtendPOVM (MA t)) ∧ (∀ (i : Fin ℓ),
hidingAliceError L w hL (Ξ.expandA (Sum.inl (none, 0))) MA' i = hidingAliceError L w hL Ξ MA i) ∧ introAliceZError projectPauli Z q (Ξ.expandA (Sum.inl (none, 0))) MA' = introAliceZError projectPauli Z q Ξ MA ∧ introBobZError projectPauli Z q (Ξ.expandA (Sum.inl (none, 0))) MB = introBobZError projectPauli Z q Ξ MB ∧ ∀ (i : Fin ℓ), hidingBobError L w hL (Ξ.expandA (Sum.inl (none, 0))) MB i = hidingBobError L w hL Ξ MB i
The actual current tests produce a projective next family and its complete prefix invariant. No selected-measurement or mixing-error bound is assumed: those are derived from the supplied current invariant. The primitive Z errors and the hiding errors of both players are unchanged on the extended model.