An adaptive dilation from the actual parsed game tests #
The three mixing errors are derived from the current game's failure, primitive Z extraction, and the fixed hiding approximation. Deterministic answer refinement retains all malformed mass. The common-ancilla residual projectors are then constructed by the proved mixing and dilation theorem.
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 Ξ, the product form is one of
POVMs in the matrices over the remaining registers with entries in its first algebra, and the
common ancilla is the dilation ancilla DilationAncilla _ K of exists_adaptive_prefix_dilation,
whose size K the theorem returns.
theorem
MIPRE.Introspection.TypedEstimates.introspect_refined_stage_bounds
{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 ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
[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) ℬ))
{ε η δ : ℝ}
(hε : 0 ≤ ε)
(hη : 0 ≤ η)
(hδ : 0 ≤ δ)
(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)
(j : Fin ℓ)
(hSA : IsPVMIn (MA (QuestionType.sample w, 0)).op)
(hSB : IsPVMIn (MB (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 ≤ η)
(hHide : IsPVMIn (MA (QuestionType.hide w j, 0)).op)
(hRead : IsPVMIn (MB (QuestionType.read w, 0)).op)
(hfine :
∑ i : Option ((ι → F) × (ι → F) × (ι → F)),
(Ξ.reg (ι → F)).xSqNorm ((POVMIn.map (hidingCoarse (L w) ↑j) (MA (QuestionType.hide w j, 0))).op i)
(smulKron 1 (Honest.hideCoarseOp (L w) (↑j) hL i)) ≤ δ)
(M :
(y : ι → F) →
POVMIn (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).op a))
(hsupport : ∀ (y x : ι → F) (a : A), (L w).outputPrefix (↑j) x ≠ y → (M y).op (some (x, a)) = 0)
:
have budget := adaptiveStageBudget (ℓ - ↑j) (↑(TypeGraph.edges E X Z ℓ).card * ε) η δ;
have R := fun (y : ι → F) (p : (Fin (Fintype.card ↥((L w).factorOfPrefix (↑j) y)) → F) × Option ((ι → F) × A)) =>
(stageAnswerRefinementPOVM (L w) (↑j) y (M y)).op p;
prefixStageMarginalError (L w) hL (↑j) Ξ R ≤ budget ∧ (prefixStageCommutatorError (L w) hL (↑j) Ξ R (fun (x : ι → F) => Weyl.wZ) fun (x : ι → F) => LinearMap.id) ≤ budget ∧ (prefixStageCommutatorError (L w) hL (↑j) Ξ R (fun (x : ι → F) => Weyl.wX) fun (y : ι → F) =>
CL.lperp (coordinateLinear (CLChecks.stageLinear (L w) (↑j) y))) ≤ budget
All three errors required by mixing follow from the actual tests and the current structural prefix invariant, under one explicit budget.
theorem
MIPRE.Introspection.TypedEstimates.exists_game_adaptive_prefix_dilation
{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 ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
[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) ℬ))
{ε η δ : ℝ}
(hε : 0 ≤ ε)
(hη : 0 ≤ η)
(hδ : 0 ≤ δ)
(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)
(j : Fin ℓ)
(hSA : IsPVMIn (MA (QuestionType.sample w, 0)).op)
(hSB : IsPVMIn (MB (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 ≤ η)
(hHide : IsPVMIn (MA (QuestionType.hide w j, 0)).op)
(hRead : IsPVMIn (MB (QuestionType.read w, 0)).op)
(hfine :
∑ i : Option ((ι → F) × (ι → F) × (ι → F)),
(Ξ.reg (ι → F)).xSqNorm ((POVMIn.map (hidingCoarse (L w) ↑j) (MA (QuestionType.hide w j, 0))).op i)
(smulKron 1 (Honest.hideCoarseOp (L w) (↑j) hL i)) ≤ δ)
(M :
(y : ι → F) →
POVMIn (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).op a))
(hsupport : ∀ (y x : ι → F) (a : A), (L w).outputPrefix (↑j) x ≠ y → (M y).op (some (x, a)) = 0)
(hM : ∀ (y : ι → F), IsPVMIn (M y).op)
(hsmall : adaptiveStageBudget (ℓ - ↑j) (↑(TypeGraph.edges E X Z ℓ).card * ε) η δ ≤ 1)
:
∃ (K : ℕ) (R : AdaptiveDilationFamily (L w) (↑j) 𝒜 (DilationAncilla (Option ((ι → F) × A)) K) (Option ((ι → F) × A)))
(hR : ∀ (y : ι → F) (z : Fin (Fintype.card ↥((L w).factorOfPrefix (↑j) y)) → F), IsPVMIn (R y z)),
∑ p : AdaptiveStageAnswer (L w) (↑j) (Option ((ι → F) × A)),
((Ξ.reg (ι → F)).expandA (Sum.inl (none, 0))).stateSqNorm
((Matrix.diagonal fun (x : DilationAncilla (Option ((ι → F) × A)) K) =>
(adaptiveOldJointPOVM (L w) hL ↑j fun (y : ι → F) => stageAnswerRefinementPOVM (L w) (↑j) y (M y)).op p) - (adaptiveReplacementPOVM (L w) hL (↑j) R hR).op p) ≤ 2 * √(56 * √(adaptiveStageBudget (ℓ - ↑j) (↑(TypeGraph.edges E X Z ℓ).card * ε) η δ))
Actual game tests construct the common-ancilla adaptive projectors. Only the current prefix product form and its answer support are structural inputs; none of the three analytic mixing estimates is assumed.