The actual game supplies the refined stage marginal bound #
The actual full Introspect measurement is refined deterministically. Its malformed mass is retained and charged to the actual reported-prefix error, which comes from the Sample tests and primitive Bob-Z extraction.
Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the extracted register state is
the register model Ξ.reg (ι → F) of a normalized auxiliary model Ξ, and the measurements are
POVMs in its algebras (the postprocessing identity in any ordered ⋆-ring).
theorem
MIPRE.Introspection.TypedEstimates.fullAnswerPrefix_introspectPair
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{A : Type u_6}
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
{ℓ : ℕ}
(P : CL.CLFun F ι ℓ)
(k : ℕ)
(a : ParsedAnswer (ι → F) A PauliAnswer)
:
theorem
MIPRE.Introspection.TypedEstimates.fullAnswerPrefix_introspect_marginal
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{A : Type u_6}
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
[DecidableEq A]
{ℓ : ℕ}
{R : Type u_10}
[Ring R]
[StarRing R]
[PartialOrder R]
[StarOrderedRing R]
(P : CL.CLFun F ι ℓ)
(k : ℕ)
(M : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) R)
(v : Option (ι → F))
:
fibSumIn (POVMIn.map introspectPair M).op (fullAnswerPrefix P k) v = (POVMIn.map (reportedPrefix P k AuxType.introspect) M).op v
Actual POVM postprocessing gives precisely the tested prefix map, including all malformed constructors.
theorem
MIPRE.Introspection.TypedEstimates.introspect_adaptive_marginal
{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]
[DecidableEq 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) ℬ))
{ε η : ℝ}
(hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε)
(q : κ → ZMod 2)
(hq : ∀ (z : κ → ZMod 2), (P Z).eval z = q)
(w : Bool)
(hL : (L w).SupportedOn Finset.univ)
(hS : IsPVMIn (MA (QuestionType.sample w, 0)).op)
(hZ :
∑ z : Option (ι → F),
(Ξ.reg (ι → F)).snorm
((Ξ.reg (ι → F)).πB
((POVMIn.map (pauliProjection projectPauli) (MB (QuestionType.pauli Z, q))).op z - smulKron 1 (readout some z))) ^ 2 ≤ η)
(j : ℕ)
(M : (y : ι → F) → Option ((ι → F) × A) → Matrix (↥(stageRemaining (L w) j y) → F) (↥(stageRemaining (L w) j y) → F) 𝒜)
(hform :
∀ (a : Option ((ι → F) × A)),
(POVMIn.map introspectPair (MA (QuestionType.introspect w, 0))).op a = ∑ y : ι → F, prefixResidualOp (L w) j y (M y a))
(hsupport : ∀ (y x : ι → F) (a : A), (L w).outputPrefix j x ≠ y → M y (some (x, a)) = 0)
:
(prefixStageMarginalError (L w) hL j Ξ fun (y : ι → F) => stageAnswerRefinement (L w) j y (M y)) ≤ 16 * η + 56 * ↑(TypeGraph.edges E X Z ℓ).card * ε
The real refined stage marginal is at most 16η + 56|E|ε.
The product form and old-prefix support are the current induction
invariant; the marginal estimate itself follows from actual game tests.