Extracting ordinary answers from terminal option-valued measurements

The adaptive invariant retains malformed answers as none. Mapping this outcome to a fixed valid answer preserves projectivity and cannot decrease the accepted mass of the original predicate. Applied to both concrete terminal invariants, this constructs an original-game strategy directly from the actual typed game, with no zero-malformed-mass assumption.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the completion of a malformed outcome is a coarse-graining of a POVM in any ordered ⋆-ring, and the acceptance comparison is between Born probabilities of an auxiliary model Ξ. The terminal measurements are played in the register model Ξ.reg (ι → F), where their valid effects are the conditionalReadouts of the auxiliary POVMs terminalAuxPOVM in the players' algebras 𝒜 and ℬ; the extracted strategy is a projective strategy of Ξ itself, which replaces the matrix statement's equality of local dimensions.

def MIPRE.Introspection.completeOptionPOVM {A : Type u_1} [Fintype A] [DecidableEq A] {R : Type u_3} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (a₀ : A) (Q : POVMIn (Option A) R) : POVMIn A R

Replace a malformed auxiliary outcome by a fixed ordinary answer.

Equations

• MIPRE.Introspection.completeOptionPOVM a₀ Q = MIPRE.POVMIn.map (fun (a : Option A) => a.getD a₀) Q

theorem MIPRE.Introspection.completeOptionPOVM_isPVM {A : Type u_1} [Fintype A] [DecidableEq A] {R : Type u_3} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (a₀ : A) (Q : POVMIn (Option A) R) (hQ : IsPVMIn Q.op) : IsPVMIn (completeOptionPOVM a₀ Q).op

theorem MIPRE.Introspection.option_valid_acceptance_le_complete {A : Type u_1} {B : Type u_2} [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (Q : POVMIn (Option A) 𝒜) (R : POVMIn (Option B) ℬ) (a₀ : A) (b₀ : B) (D : A → B → Bool) : ∑ a : A, ∑ b : B, (if D a b = true then 1 else 0) * Ψ.bornProb (Q.op (some a)) (R.op (some b)) ≤ ∑ a : A, ∑ b : B, (if D a b = true then 1 else 0) * Ψ.bornProb ((completeOptionPOVM a₀ Q).op a) ((completeOptionPOVM b₀ R).op b)

Accepted valid outcomes remain accepted after completion; all newly accepted malformed outcomes contribute nonnegative Born probabilities.

theorem MIPRE.Introspection.readoutAcceptance_le_completedValue {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 𝒞 𝒜 ℬ) (Q : X → POVMIn (Option A) 𝒜) (R : Y → POVMIn (Option B) ℬ) (a₀ : A) (b₀ : B) : readoutAcceptance f g Ξ (fun (x : X) (a : A) => (Q x).op (some a)) (fun (y : Y) (b : B) => (R y).op (some b)) G.D ≤ Ξ.povmValue G (fun (x : X) => completeOptionPOVM a₀ (Q x)) fun (y : Y) => completeOptionPOVM b₀ (R y)

The actual question law converts the valid part of the readout test into a lower bound on the completed ordinary-answer strategy.

theorem MIPRE.Introspection.introspectPair_map_some {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PauliAnswer : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PauliAnswer] {R : Type u_5} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (N : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) R) (y : ι → F) (a : A) : (POVMIn.map TypedEstimates.introspectPair N).op (some (y, a)) = N.op (ParsedAnswer.pair y a)

A valid full-option outcome has a unique parsed-answer preimage.

theorem MIPRE.Introspection.IntroPrefixInvariant.terminal_parsed_pair {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PauliAnswer : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PauliAnswer] {ℓ : ℕ} {𝒜 : Type u_5} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {P : CL.CLFun F ι ℓ} {N : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜)} (I : IntroPrefixInvariant P ℓ (POVMIn.map TypedEstimates.introspectPair N)) (hP : P.ExactlyOn Finset.univ) (y : ι → F) (a : A) : N.op (ParsedAnswer.pair y a) = conditionalReadout P.eval (fun (y : ι → F) (a : A) => (terminalAuxPOVM hP I y).op (some a)) (y, a)

The valid parsed effects of an actual terminal invariant have the precise conditional readout form, regardless of malformed effects.

theorem MIPRE.Introspection.TypedExtraction.exists_strategy_of_terminal_invariants {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] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] [DecidableEq A] [Nonempty A] [Fintype PauliAnswer] {ℓ : ℕ} {𝒞 : Type u_7} {𝒜 : Type u_8} {ℬ : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [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 ι ℓ) (hL : ∀ (w : Bool), (L w).ExactlyOn Finset.univ) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool) (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) (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) ℬ)) (IA : IntroPrefixInvariant (L false) ℓ (POVMIn.map TypedEstimates.introspectPair (MA (QuestionType.introspect false, 0)))) (IB : IntroPrefixInvariant (L true) ℓ (POVMIn.map TypedEstimates.introspectPair (MB (QuestionType.introspect true, 0)))) {ε : ℝ} (hfail : 1 - (Ξ.reg (ι → F)).povmValue (TypedEstimates.parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε) : ∃ (S : Ξ.ProjStrat G), 1 - ↑(TypeGraph.edges E X Z ℓ).card * ε ≤ S.value

Both concrete terminal invariants construct an ordinary-answer original strategy, a projective strategy of the auxiliary model. Completing malformed outcomes costs no additional failure.