Extracting the original strategy from introspective readouts

This proves the final game-value calculation in the soundness proof of introspection.tex. Once the induction has produced a question readout tensored with an auxiliary measurement depending on that question, the original strategy uses precisely those auxiliary measurements and the auxiliary state. The value identity below is exact, including the question-distribution normalization.

In the register model Ξ.reg I (Phase 4 of planning/mipco-track.md): the readout of the question tensored with an auxiliary operator P of the ancilla is smulKron P (readout f x), and the extracted strategy is a projective strategy of the ancillary model Ξ itself.

def MIPRE.Introspection.conditionalReadout {I : Type u_1} {X : Type u_2} {A : Type u_4} [DecidableEq I] [DecidableEq X] {R : Type u_9} [Ring R] [Algebra ℂ R] (f : I → X) (P : X → A → R) (xa : X × A) : Matrix I I R

Read the question from the EPR seed and then measure the auxiliary system.

Equations

• MIPRE.Introspection.conditionalReadout f P xa = MIPRE.smulKron (P xa.1 xa.2) (MIPRE.Introspection.readout f xa.1)

theorem MIPRE.Introspection.conditionalReadout_isPVM {I : Type u_1} {X : Type u_2} {A : Type u_4} [Fintype I] [DecidableEq I] [Fintype X] [DecidableEq X] [Fintype A] [DecidableEq A] {R : Type u_9} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (f : I → X) (P : X → A → R) (hP : ∀ (x : X), IsPVMIn (P x)) : IsPVMIn (conditionalReadout f P)

The question-dependent auxiliary family gives an actual joint PVM.

theorem MIPRE.Introspection.bornProb_conditionalReadout {I : Type u_1} {X : Type u_2} {Y : Type u_3} {A : Type u_4} {B : Type u_5} [Fintype I] [DecidableEq I] [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] {𝒞 : Type u_6} {𝒜 : Type u_7} {ℬ : Type u_8} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (f : I → X) (g : I → Y) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (P : X → A → 𝒜) (Q : Y → B → ℬ) (xa : X × A) (yb : Y × B) : (Ξ.reg I).bornProb (conditionalReadout f P xa) (conditionalReadout g Q yb) = SampledGame.dist f g xa.1 yb.1 * Ξ.bornProb (P xa.1 xa.2) (Q yb.1 yb.2)

The full joint answer probability factors into the original question law and the auxiliary strategy's conditional answer probability.

noncomputable def MIPRE.Introspection.readoutAcceptance {I : Type u_1} {X : Type u_2} {Y : Type u_3} {A : Type u_4} {B : Type u_5} [Fintype I] [DecidableEq I] [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype A] [Fintype B] {𝒞 : Type u_6} {𝒜 : Type u_7} {ℬ : Type u_8} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (f : I → X) (g : I → Y) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (P : X → A → 𝒜) (Q : Y → B → ℬ) (D : X → Y → A → B → Bool) : ℝ

Acceptance probability of the introspective test on the terminal measurements.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Introspection.readoutAcceptance_eq_value {I : Type u_1} {X : Type u_2} {Y : Type u_3} {A : Type u_4} {B : Type u_5} [Fintype I] [DecidableEq I] [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] {𝒞 : Type u_6} {𝒜 : Type u_7} {ℬ : Type u_8} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (G : Game X Y A B) (f : I → X) (g : I → Y) (hμ : ∀ (x : X) (y : Y), G.μ x y = SampledGame.dist f g x y) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (S : Ξ.ProjStrat G) : readoutAcceptance f g Ξ (fun (x : X) (a : A) => (S.PA x).op a) (fun (y : Y) (b : B) => (S.PB y).op b) G.D = S.value

The terminal readout acceptance is the value of the actual auxiliary strategy.

theorem MIPRE.Introspection.val_ge_of_readoutAcceptance {I : Type u_1} [Fintype I] [DecidableEq I] {𝒞 : Type u_6} {𝒜 : Type u_7} {ℬ : Type u_8} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {X Y A B : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] (G : Game X Y A B) (f : I → X) (g : I → Y) (hμ : ∀ (x : X) (y : Y), G.μ x y = SampledGame.dist f g x y) {ω : ValueModel} (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hω : ω.Dominates Ξ) (S : Ξ.ProjStrat G) (ε : ℝ) (h : 1 - ε ≤ readoutAcceptance f g Ξ (fun (x : X) (a : A) => (S.PA x).op a) (fun (y : Y) (b : B) => (S.PB y).op b) G.D) : 1 - ε ≤ ω.val G

No further error or dimension factor is lost in the final extraction step: the value of a value model dominating the auxiliary model is at least the acceptance.

def MIPRE.Introspection.extractedStrategy {X : Type u_2} {Y : Type u_3} {A : Type u_4} {B : Type u_5} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {𝒞 : Type u_6} {𝒜 : Type u_7} {ℬ : Type u_8} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (G : Game X Y A B) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (P : X → A → 𝒜) (Q : Y → B → ℬ) (hP : ∀ (x : X), IsPVMIn (P x)) (hQ : ∀ (y : Y), IsPVMIn (Q y)) : Ξ.ProjStrat G

The extracted strategy keeps the auxiliary model and its question-indexed measurements, discarding the EPR register used to generate the questions.

Equations

• MIPRE.Introspection.extractedStrategy G Ξ hΞ P Q hP hQ = { PA := fun (x : X) => ⋯.toPOVMIn, PB := fun (y : Y) => ⋯.toPOVMIn, projA := ⋯, projB := ⋯, ψ_unit := hΞ }

theorem MIPRE.Introspection.exists_strategy_of_readoutAcceptance {I : Type u_1} {X : Type u_2} {Y : Type u_3} {A : Type u_4} {B : Type u_5} [Fintype I] [DecidableEq I] [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] {𝒞 : Type u_6} {𝒜 : Type u_7} {ℬ : Type u_8} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (G : Game X Y A B) (f : I → X) (g : I → Y) (hμ : ∀ (x : X) (y : Y), G.μ x y = SampledGame.dist f g x y) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (P : X → A → 𝒜) (Q : Y → B → ℬ) (hP : ∀ (x : X), IsPVMIn (P x)) (hQ : ∀ (y : Y), IsPVMIn (Q y)) : ∃ (S : Ξ.ProjStrat G), S.value = readoutAcceptance f g Ξ P Q G.D

The final introspection test directly certifies an equally good projective strategy for the original game, in the auxiliary model.

theorem MIPRE.Introspection.verifier_readoutAcceptance_eq_value {𝒞 : Type u_6} {𝒜 : Type u_7} {ℬ : Type u_8} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (S : Ξ.ProjStrat (V.game n T)) : readoutAcceptance (V.sampler.cl n Player.alice).eval (V.sampler.cl n Player.bob).eval Ξ (fun (x : Fin (V.sampler.dim n) → CL.𝔽₂) (a : Verifier.Answers T) => (S.PA x).op a) (fun (y : Fin (V.sampler.dim n) → CL.𝔽₂) (b : Verifier.Answers T) => (S.PB y).op b) (V.game n T).D = S.value

Specialization to the actual game of a normal-form verifier: there is no unproved distribution-identification hypothesis at this interface.