Decoding the actual compiled strategy into the canonical finite game

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): decoding is question-dependent answer merging of a projective strategy in any model (ProjStrat.mergeAnswersByQuestion), so the decoded strategy lives in the same model.

@[reducible, inline]

abbrev MIPRE.Introspection.CanonicalDecoded.Question (c lam n : ℕ) : Type

Equations

• MIPRE.Introspection.CanonicalDecoded.Question c lam n = MIPRE.CL.Detyping.Question MIPRE.Introspection.DecisionKernel.Label (Fin (MIPRE.Introspection.PauliSampler.dimension c lam n))

noncomputable def MIPRE.Introspection.CanonicalDecoded.decode (c lam n : ℕ) (q : Question c lam n) (a : Verifier.Answers (DecisionCompiler.outerBound c lam n)) : ParsedAnswer (Fin (SourceCompiler.registerBits c lam n) → CL.𝔽₂) (Verifier.Answers ((2 ^ n) ^ lam)) (QLD.Answer (CanonicalGame.field c lam n).carrier (SourceCompiler.registerPower c lam n) 1)

Decode each bounded binary answer according to its own question type.

Equations

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

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.CanonicalDecoded.strategy {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (lam n : ℕ) (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ SourceCompiler.registerBits c lam n) (S : M.ProjStrat (DecisionCompiler.rawGame c hc he U (V.sampler.prog, V.decider.prog) lam n)) : M.ProjStrat (CanonicalGame.quotient c hc he lam n V hs)

Equations

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

theorem MIPRE.Introspection.CanonicalDecoded.accepts (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) {lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hc2 : 2 ≤ c) (hs : V.sampler.dim (2 ^ n) ≤ SourceCompiler.registerBits c lam n) (q r : Question c lam n) (a b : Verifier.Answers (DecisionCompiler.outerBound c lam n)) (h : (DecisionCompiler.rawGame c hc he U (V.sampler.prog, V.decider.prog) lam n).D q r a b = true) : (CanonicalGame.quotient c hc he lam n V hs).D q r (decode c lam n q a) (decode c lam n r b) = true

Kernel acceptance is preserved by this total, finite answer decoding.

theorem MIPRE.Introspection.CanonicalDecoded.value_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) {lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hc2 : 2 ≤ c) (hs : V.sampler.dim (2 ^ n) ≤ SourceCompiler.registerBits c lam n) (S : M.ProjStrat (DecisionCompiler.rawGame c hc he U (V.sampler.prog, V.decider.prog) lam n)) : S.value ≤ (strategy c hc he U lam n V hs S).value

Decoding preserves the question law and cannot lower the strategy value.

theorem MIPRE.Introspection.CanonicalDecoded.failure_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) {lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hc2 : 2 ≤ c) (hs : V.sampler.dim (2 ^ n) ≤ SourceCompiler.registerBits c lam n) (S : M.ProjStrat (DecisionCompiler.rawGame c hc he U (V.sampler.prog, V.decider.prog) lam n)) {ε : ℝ} (hS : 1 - S.value ≤ ε) : 1 - (strategy c hc he U lam n V hs S).value ≤ ε

theorem MIPRE.Introspection.CanonicalDecoded.measurement_supported (c lam n : ℕ) {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : Question c lam n → POVMIn (Verifier.Answers (DecisionCompiler.outerBound c lam n)) R) (W : QLD.Bas) (a : ParsedAnswer (Fin (SourceCompiler.registerBits c lam n) → CL.𝔽₂) (Verifier.Answers ((2 ^ n) ^ lam)) (QLD.Answer (CanonicalGame.field c lam n).carrier (SourceCompiler.registerPower c lam n) 1)) : (POVMIn.map (decode c lam n (Sum.inl (QLD.Ty.pauli W), 0)) (P (Sum.inl (QLD.Ty.pauli W), 0))).op a ≠ 0 → ∃ (x : (Fin (SourceCompiler.registerPower c lam n) → Bool) → (CanonicalGame.field c lam n).carrier), a = ParsedAnswer.pauli (QLD.Answer.pauliAns x)

theorem MIPRE.Introspection.CanonicalDecoded.supported_A {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (lam n : ℕ) (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ SourceCompiler.registerBits c lam n) (S : M.ProjStrat (DecisionCompiler.rawGame c hc he U (V.sampler.prog, V.decider.prog) lam n)) (W : QLD.Bas) (a : ParsedAnswer (Fin (2 ^ SourceCompiler.registerPower c lam n * SourceCompiler.fieldBits c lam n) → ZMod 2) (Verifier.Answers ((2 ^ n) ^ lam)) (QLD.Answer (CanonicalGame.field c lam n).carrier (SourceCompiler.registerPower c lam n) 1)) : ((strategy c hc he U lam n V hs S).PA (Sum.inl (QLD.Ty.pauli W), 0)).op a ≠ 0 → ∃ (x : (Fin (SourceCompiler.registerPower c lam n) → Bool) → (CanonicalGame.field c lam n).carrier), a = ParsedAnswer.pauli (QLD.Answer.pauliAns x)

Full Pauli effects are supported on genuine full Pauli outcomes for Alice.

theorem MIPRE.Introspection.CanonicalDecoded.supported_B {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (lam n : ℕ) (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ SourceCompiler.registerBits c lam n) (S : M.ProjStrat (DecisionCompiler.rawGame c hc he U (V.sampler.prog, V.decider.prog) lam n)) (W : QLD.Bas) (a : ParsedAnswer (Fin (2 ^ SourceCompiler.registerPower c lam n * SourceCompiler.fieldBits c lam n) → ZMod 2) (Verifier.Answers ((2 ^ n) ^ lam)) (QLD.Answer (CanonicalGame.field c lam n).carrier (SourceCompiler.registerPower c lam n) 1)) : ((strategy c hc he U lam n V hs S).PB (Sum.inl (QLD.Ty.pauli W), 0)).op a ≠ 0 → ∃ (x : (Fin (SourceCompiler.registerPower c lam n) → Bool) → (CanonicalGame.field c lam n).carrier), a = ParsedAnswer.pauli (QLD.Answer.pauliAns x)

Full Pauli effects are supported on genuine full Pauli outcomes for Bob.