Exact normalization of the Introspect answer format

All malformed Introspect constructors are already rejected by the parsed predicate. They may therefore be merged into one malformed representative, without assuming that their effects vanish and without changing game value. The normalized measurement factors exactly through its full option-valued question/answer report, and preserves that report and projectivity.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the measurements are POVMs in any ordered ⋆-ring, and the value identity holds in any bipartite model.

def MIPRE.Introspection.restoreIntroAnswer {V : Type u_1} {A : Type u_2} {PauliAnswer : Type u_3} [Zero V] : Option (V × A) → ParsedAnswer V A PauliAnswer

A fixed malformed representative avoids any inhabitedness requirement on the source-answer and Pauli-answer alphabets.

Equations

• MIPRE.Introspection.restoreIntroAnswer none = MIPRE.Introspection.ParsedAnswer.hide 0 0 0
• MIPRE.Introspection.restoreIntroAnswer (some p) = MIPRE.Introspection.ParsedAnswer.pair p.1 p.2

@[simp]

theorem MIPRE.Introspection.introspectPair_restoreIntroAnswer {A : Type u_2} {PauliAnswer : Type u_3} {F : Type u_4} {ι : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] (a : Option ((ι → F) × A)) : TypedEstimates.introspectPair (restoreIntroAnswer a) = a

def MIPRE.Introspection.canonicalIntroAnswer {A : Type u_2} {PauliAnswer : Type u_3} {F : Type u_4} {ι : Type u_5} [Field F] (a : ParsedAnswer (ι → F) A PauliAnswer) : ParsedAnswer (ι → F) A PauliAnswer

Equations

• MIPRE.Introspection.canonicalIntroAnswer a = MIPRE.Introspection.restoreIntroAnswer (MIPRE.Introspection.TypedEstimates.introspectPair a)

@[simp]

theorem MIPRE.Introspection.introspectPair_canonicalIntroAnswer {A : Type u_2} {PauliAnswer : Type u_3} {F : Type u_4} {ι : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] (a : ParsedAnswer (ι → F) A PauliAnswer) : TypedEstimates.introspectPair (canonicalIntroAnswer a) = TypedEstimates.introspectPair a

theorem MIPRE.Introspection.check_canonicalIntroAnswer_left {A : Type u_2} {PauliAnswer : Type u_3} {F : Type u_4} {ι : Type u_5} {PauliType : Type u_6} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) (t : QuestionType PauliType ℓ) (a b : ParsedAnswer (ι → F) A PauliAnswer) : TypedPredicate.check L X Z projectPauli D DP (QuestionType.introspect w) t (canonicalIntroAnswer a) b = TypedPredicate.check L X Z projectPauli D DP (QuestionType.introspect w) t a b

noncomputable def MIPRE.Introspection.canonicalizeIntro {A : Type u_2} {PauliAnswer : Type u_3} {F : Type u_4} {ι : Type u_5} {PauliType : Type u_6} {κ : Type u_7} {R : Type u_8} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [DecidableEq PauliType] [Fintype κ] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Fintype A] [Fintype PauliAnswer] {ℓ : ℕ} (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) R) (w : Bool) (q : QuestionType PauliType ℓ × (κ → ZMod 2)) : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) R

The actual family changes only the selected zero-content Introspect question, by deterministic postprocessing of its old answer.

Equations

• MIPRE.Introspection.canonicalizeIntro MA w q = if q = (MIPRE.Introspection.QuestionType.introspect w, 0) then MIPRE.POVMIn.map MIPRE.Introspection.canonicalIntroAnswer (MA q) else MA q

theorem MIPRE.Introspection.canonicalizeIntro_at {A : Type u_2} {PauliAnswer : Type u_3} {F : Type u_4} {ι : Type u_5} {PauliType : Type u_6} {κ : Type u_7} {R : Type u_8} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Fintype A] [Fintype PauliAnswer] {ℓ : ℕ} (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) R) (w : Bool) : canonicalizeIntro MA w (QuestionType.introspect w, 0) = POVMIn.map canonicalIntroAnswer (MA (QuestionType.introspect w, 0))

theorem MIPRE.Introspection.canonicalizeIntro_other {A : Type u_2} {PauliAnswer : Type u_3} {F : Type u_4} {ι : Type u_5} {PauliType : Type u_6} {κ : Type u_7} {R : Type u_8} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Fintype A] [Fintype PauliAnswer] {ℓ : ℕ} (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) R) (w : Bool) (q : CL.Detyping.Question (QuestionType PauliType ℓ) κ) (hq : q ≠ (QuestionType.introspect w, 0)) : canonicalizeIntro MA w q = MA q

theorem MIPRE.Introspection.canonicalizeIntro_factor {A : Type u_2} {PauliAnswer : Type u_3} {F : Type u_4} {ι : Type u_5} {PauliType : Type u_6} {κ : Type u_7} {R : Type u_8} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Fintype A] [Fintype PauliAnswer] {ℓ : ℕ} (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) R) (w : Bool) : canonicalizeIntro MA w (QuestionType.introspect w, 0) = POVMIn.map restoreIntroAnswer (POVMIn.map TypedEstimates.introspectPair (MA (QuestionType.introspect w, 0)))

theorem MIPRE.Introspection.canonicalizeIntro_isPVM {A : Type u_2} {PauliAnswer : Type u_3} {F : Type u_4} {ι : Type u_5} {PauliType : Type u_6} {κ : Type u_7} {R : Type u_8} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype PauliType] [DecidableEq PauliType] [Fintype κ] [DecidableEq κ] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Fintype A] [Fintype PauliAnswer] {ℓ : ℕ} (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) R) (w : Bool) (hMA : ∀ (q : CL.Detyping.Question (QuestionType PauliType ℓ) κ), IsPVMIn (MA q).op) (q : CL.Detyping.Question (QuestionType PauliType ℓ) κ) : IsPVMIn (canonicalizeIntro MA w q).op

theorem MIPRE.Introspection.TypedEstimates.canonicalizeIntro_condWin {F : Type u_4} {ι : Type u_5} {PauliType : Type u_6} {PauliAnswer : Type u_7} {κ : Type u_8} {A : Type u_9} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Fintype A] [Fintype κ] [DecidableEq κ] {ℓ : ℕ} {𝒞 : Type u_10} {𝒜 : Type u_11} {ℬ : Type u_12} [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) (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 𝒞 𝒜 ℬ) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) 𝒜) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) ℬ) (w : Bool) (q r : CL.Detyping.Question (QuestionType PauliType ℓ) κ) : Ψ.condWin (parsedGame E X Z P L projectPauli D DP) (canonicalizeIntro MA w) MB q r = Ψ.condWin (parsedGame E X Z P L projectPauli D DP) MA MB q r

theorem MIPRE.Introspection.TypedEstimates.canonicalizeIntro_value {F : Type u_4} {ι : Type u_5} {PauliType : Type u_6} {PauliAnswer : Type u_7} {κ : Type u_8} {A : Type u_9} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Fintype A] [Fintype κ] [DecidableEq κ] {ℓ : ℕ} {𝒞 : Type u_10} {𝒜 : Type u_11} {ℬ : Type u_12} [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) (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 𝒞 𝒜 ℬ) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) 𝒜) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) ℬ) (w : Bool) : Ψ.povmValue (parsedGame E X Z P L projectPauli D DP) (canonicalizeIntro MA w) MB = Ψ.povmValue (parsedGame E X Z P L projectPauli D DP) MA MB

Format normalization has exactly the original parsed-game value, including the entire malformed-answer mass.