Final extraction from the actual typed introspection game #
This is the last game calculation in introspection.tex: the cross-introspection
edge has probability exactly 1 / |E|, accepts precisely the original predicate
on pair answers, and rejects all other constructors. Consequently terminal
readout measurements yield an actual original-game strategy with failure at
most |E| times the typed-game failure. The tensor-product form is the output
required of the hiding induction; no separate acceptance premise is assumed.
Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the typed game is played in a
model Ψ, the terminal measurements in the register model Ξ.reg (ι → F), where the product form
of a readout is conditionalReadout (smulKron of the auxiliary operator and the question
readout). The extracted strategy is a projective strategy of the auxiliary model Ξ itself, which
replaces the matrix statement's equality of local dimensions; the actual state of the last theorem
is a unit vector φ of the register model's space, played in (Ξ.reg (ι → F)).withState φ.
theorem
MIPRE.Introspection.TypedExtraction.cross_check
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{A : Type u_6}
[Fintype PauliType]
[DecidableEq PauliType]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
[Fintype PauliAnswer]
{ℓ : ℕ}
(L : Bool → CL.CLFun F ι ℓ)
(X Z : PauliType)
(projectPauli : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool)
(a b : ParsedAnswer (ι → F) A PauliAnswer)
:
TypedPredicate.check L X Z projectPauli D DP (QuestionType.introspect false) (QuestionType.introspect true) a b = match a, b with
| ParsedAnswer.pair x a, ParsedAnswer.pair y b => D x y a b
| x, x_1 => false
An accepted cross-introspection answer has the pair constructor on each side.
theorem
MIPRE.Introspection.TypedExtraction.sum_pairs
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{A : Type u_6}
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
[Fintype PauliAnswer]
{R : Type u_7}
[AddCommMonoid R]
(f : ParsedAnswer (ι → F) A PauliAnswer → R)
(hp : ∀ (p : PauliAnswer), f (ParsedAnswer.pauli p) = 0)
(hr : ∀ (x y : ι → F) (a : A), f (ParsedAnswer.read x y a) = 0)
(hh : ∀ (x y z : ι → F), f (ParsedAnswer.hide x y z) = 0)
:
A sum supported on the pair answers is exactly a sum over their two components.
def
MIPRE.Introspection.TypedExtraction.pairReadout
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{A : Type u_6}
[DecidableEq F]
[Fintype ι]
{R : Type u_7}
[Ring R]
[Algebra ℂ R]
(f : (ι → F) → ι → F)
(Q : (ι → F) → A → R)
:
ParsedAnswer (ι → F) A PauliAnswer → Matrix (ι → F) (ι → F) R
Embed the terminal question/answer PVM into the full parsed alphabet.
Equations
Instances For
theorem
MIPRE.Introspection.TypedExtraction.pairReadout_isPVM
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{A : Type u_6}
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
[Fintype PauliAnswer]
{R : Type u_7}
[Ring R]
[StarRing R]
[Algebra ℂ R]
[StarModule ℂ R]
(f : (ι → F) → ι → F)
(Q : (ι → F) → A → R)
(hQ : ∀ (y : ι → F), IsPVMIn (Q y))
:
IsPVMIn (pairReadout f Q)
The terminal pair effects and zero effects on other constructors form a genuine PVM.
theorem
MIPRE.Introspection.TypedExtraction.condWin_cross_eq
{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]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
[DecidableEq A]
[Fintype PauliAnswer]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[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) ℬ)
:
Ψ.condWin (TypedEstimates.parsedGame E X Z P L projectPauli D DP) MA MB (QuestionType.introspect false, 0)
(QuestionType.introspect true, 0) = ∑ xa : (ι → F) × A,
∑ yb : (ι → F) × A,
(if D xa.1 yb.1 xa.2 yb.2 = true then 1 else 0) * Ψ.bornProb ((MA (QuestionType.introspect false, 0)).op (ParsedAnswer.pair xa.1 xa.2))
((MB (QuestionType.introspect true, 0)).op (ParsedAnswer.pair yb.1 yb.2))
On the concrete game edge, only pair answers contribute to the conditional value.
theorem
MIPRE.Introspection.TypedExtraction.cross_failure_le
{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]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
[DecidableEq A]
[Fintype PauliAnswer]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[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 𝒞 𝒜 ℬ)
(hΨ : ‖Ψ.ψ‖ = 1)
(MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) 𝒜)
(MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) ℬ)
{ε : ℝ}
(hfail : 1 - Ψ.povmValue (TypedEstimates.parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε)
:
Ψ.condFail (TypedEstimates.parsedGame E X Z P L projectPauli D DP) MA MB (QuestionType.introspect false, 0)
(QuestionType.introspect true, 0) ≤ ↑(TypeGraph.edges E X Z ℓ).card * ε
The actual typed game's success bounds the conditional cross-test failure.
theorem
MIPRE.Introspection.TypedExtraction.condWin_cross_readout
{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]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
[DecidableEq A]
[Fintype PauliAnswer]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[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)
[StarProper 𝒜]
[StarProper ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(QA : (ι → F) → A → 𝒜)
(QB : (ι → F) → A → ℬ)
(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) ℬ))
(hA :
∀ (y : ι → F) (a : A),
(MA (QuestionType.introspect false, 0)).op (ParsedAnswer.pair y a) = conditionalReadout (L false).eval QA (y, a))
(hB :
∀ (y : ι → F) (a : A),
(MB (QuestionType.introspect true, 0)).op (ParsedAnswer.pair y a) = conditionalReadout (L true).eval QB (y, a))
:
(Ξ.reg (ι → F)).condWin (TypedEstimates.parsedGame E X Z P L projectPauli D DP) MA MB (QuestionType.introspect false, 0)
(QuestionType.introspect true, 0) = readoutAcceptance (L false).eval (L true).eval Ξ QA QB D
Terminal pair effects of product form identify the conditional value exactly, in the register model. No premise about the other parsed constructors is needed: the decider rejects them.
theorem
MIPRE.Introspection.TypedExtraction.exists_strategy_of_terminal_form
{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]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
[DecidableEq A]
[Fintype PauliAnswer]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[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)
[StarProper 𝒜]
[StarProper ℬ]
(G : Game (ι → F) (ι → F) A A)
(hμ : ∀ (x y : ι → F), G.μ x y = CL.clDist (L false).eval (L true).eval x y)
(hD : G.D = D)
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(hΞ : ‖Ξ.ψ‖ = 1)
(QA : (ι → F) → A → 𝒜)
(QB : (ι → F) → A → ℬ)
(hQA : ∀ (x : ι → F), IsPVMIn (QA x))
(hQB : ∀ (y : ι → F), IsPVMIn (QB y))
(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) ℬ))
(hA :
∀ (y : ι → F) (a : A),
(MA (QuestionType.introspect false, 0)).op (ParsedAnswer.pair y a) = conditionalReadout (L false).eval QA (y, a))
(hB :
∀ (y : ι → F) (a : A),
(MB (QuestionType.introspect true, 0)).op (ParsedAnswer.pair y a) = conditionalReadout (L true).eval QB (y, a))
{ε : ℝ}
(hfail : 1 - (Ξ.reg (ι → F)).povmValue (TypedEstimates.parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε)
:
The final extraction step from the actual game. Given the product forms
produced by the hiding induction, near-perfect typed play constructs a legal
original strategy in exactly the auxiliary model, with explicit loss |E| ε.
theorem
MIPRE.Introspection.TypedExtraction.exists_strategy_of_approx_terminal_form
{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]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
[DecidableEq A]
[Fintype PauliAnswer]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[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)
[StarProper 𝒜]
[StarProper ℬ]
[StarModule ℂ 𝒜]
[StarModule ℂ ℬ]
(G : Game (ι → F) (ι → F) A A)
(hμ : ∀ (x y : ι → F), G.μ x y = CL.clDist (L false).eval (L true).eval x y)
(hD : G.D = D)
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(hΞ : ‖Ξ.ψ‖ = 1)
(QA : (ι → F) → A → 𝒜)
(QB : (ι → F) → A → ℬ)
(hQA : ∀ (x : ι → F), IsPVMIn (QA x))
(hQB : ∀ (y : ι → F), IsPVMIn (QB y))
(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 : IsPVMIn (MA (QuestionType.introspect false, 0)).op)
(hMB : IsPVMIn (MB (QuestionType.introspect true, 0)).op)
{ε δA δB : ℝ}
(hfail : 1 - (Ξ.reg (ι → F)).povmValue (TypedEstimates.parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε)
(hA :
∑ a : ParsedAnswer (ι → F) A PauliAnswer,
(Ξ.reg (ι → F)).stateSqNorm ((MA (QuestionType.introspect false, 0)).op a - pairReadout (L false).eval QA a) ≤ δA)
(hB :
∑ b : ParsedAnswer (ι → F) A PauliAnswer,
(Ξ.reg (ι → F)).swap.stateSqNorm ((MB (QuestionType.introspect true, 0)).op b - pairReadout (L true).eval QB b) ≤ δB)
:
Quantitative terminal extraction. The induction need only approximate
the pair readouts in summed squared state distance. Its two errors cost exactly
2 sqrt(deltaA) + 2 sqrt(deltaB) after the cross-test's |E| epsilon loss.
The actual measurements may have effects on all malformed constructors.
theorem
MIPRE.Introspection.TypedExtraction.exists_strategy_of_state_and_terminal_approx
{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]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
[DecidableEq A]
[Fintype PauliAnswer]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[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)
[StarProper 𝒜]
[StarProper ℬ]
[StarModule ℂ 𝒜]
[StarModule ℂ ℬ]
(G : Game (ι → F) (ι → F) A A)
(hμ : ∀ (x y : ι → F), G.μ x y = CL.clDist (L false).eval (L true).eval x y)
(hD : G.D = D)
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(hΞ : ‖Ξ.ψ‖ = 1)
(φ : (Ξ.reg (ι → F)).H)
(hφ : ‖φ‖ = 1)
(QA : (ι → F) → A → 𝒜)
(QB : (ι → F) → A → ℬ)
(hQA : ∀ (x : ι → F), IsPVMIn (QA x))
(hQB : ∀ (y : ι → F), IsPVMIn (QB y))
(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)
{ε η δA δB : ℝ}
(hfail : 1 - ((Ξ.reg (ι → F)).withState φ).povmValue (TypedEstimates.parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε)
(hstate : ‖φ - (Ξ.reg (ι → F)).ψ‖ ^ 2 ≤ η)
(hA :
∑ a : ParsedAnswer (ι → F) A PauliAnswer,
(Ξ.reg (ι → F)).stateSqNorm ((MA (QuestionType.introspect false, 0)).op a - pairReadout (L false).eval QA a) ≤ δA)
(hB :
∑ b : ParsedAnswer (ι → F) A PauliAnswer,
(Ξ.reg (ι → F)).swap.stateSqNorm ((MB (QuestionType.introspect true, 0)).op b - pairReadout (L true).eval QB b) ≤ δB)
:
The complete final extraction calculation after Pauli state approximation and hiding measurement approximation. All three errors are paid explicitly.