Actual Pauli strategies extracted by restricting introspection

The strategy is built on exactly the original finite registers and state. Outer malformed answers are completed at fixed answers; the binary CL strategy then pulls back to the actual QLD game along canonical encodings.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the strategies are projective strategies of one model Ξ, and the restricted QLD strategy is a strategy of the same model, so the state is unchanged by construction.

noncomputable def MIPRE.Introspection.PauliRestriction.pauliCheck {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (p q : QLD.Ty) (x y : Fin ((3 * m + 3) * t) → ZMod 2) : QLD.Answer F m d → QLD.Answer F m d → Bool

Equations

• MIPRE.Introspection.PauliRestriction.pauliCheck hm b p q x y = MIPRE.QLD.accepts hm (MIPRE.QLD.PauliCL.binaryQuestion b p x) (MIPRE.QLD.PauliCL.binaryQuestion b q y)

noncomputable def MIPRE.Introspection.PauliRestriction.fullGame {F : Type u_1} {F₀ : Type u_2} {ι : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Field F₀] [Fintype F₀] [Fintype ι] [DecidableEq ι] [Fintype A] {m t d ℓ : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun F₀ ι ℓ) (project : QLD.Answer F m d → ι → F₀) (D : (ι → F₀) → (ι → F₀) → A → A → Bool) : Game (CL.Detyping.Question (QuestionType QLD.Ty ℓ) (Fin ((3 * m + 3) * t))) (CL.Detyping.Question (QuestionType QLD.Ty ℓ) (Fin ((3 * m + 3) * t))) (ParsedAnswer (ι → F₀) A (QLD.Answer F m d)) (ParsedAnswer (ι → F₀) A (QLD.Answer F m d))

Equations

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

def MIPRE.Introspection.PauliRestriction.alice {F : Type u_1} {F₀ : Type u_2} {ι : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Field F₀] [Fintype F₀] [Fintype ι] [DecidableEq ι] [Fintype A] {m t d ℓ : ℕ} [NeZero m] {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] {Ξ : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun F₀ ι ℓ) (project : QLD.Answer F m d → ι → F₀) (D : (ι → F₀) → (ι → F₀) → A → A → Bool) (S : Ξ.ProjStrat (fullGame hm b L project D)) (a₀ : QLD.Answer F m d) (q : QLD.PauliCL.BinaryQuestion m t) : POVMIn (QLD.Answer F m d) 𝒜

Equations

• MIPRE.Introspection.PauliRestriction.alice hm b L project D S a₀ q = MIPRE.Introspection.completePauliPOVM a₀ (S.PA (Sum.inl q.1, q.2))

def MIPRE.Introspection.PauliRestriction.bob {F : Type u_1} {F₀ : Type u_2} {ι : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Field F₀] [Fintype F₀] [Fintype ι] [DecidableEq ι] [Fintype A] {m t d ℓ : ℕ} [NeZero m] {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ξ : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun F₀ ι ℓ) (project : QLD.Answer F m d → ι → F₀) (D : (ι → F₀) → (ι → F₀) → A → A → Bool) (S : Ξ.ProjStrat (fullGame hm b L project D)) (b₀ : QLD.Answer F m d) (q : QLD.PauliCL.BinaryQuestion m t) : POVMIn (QLD.Answer F m d) ℬ

Equations

• MIPRE.Introspection.PauliRestriction.bob hm b L project D S b₀ q = MIPRE.Introspection.completePauliPOVM b₀ (S.PB (Sum.inl q.1, q.2))

theorem MIPRE.Introspection.PauliRestriction.alice_isPVM {F : Type u_1} {F₀ : Type u_2} {ι : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Field F₀] [Fintype F₀] [DecidableEq F₀] [Fintype ι] [DecidableEq ι] [Fintype A] {m t d ℓ : ℕ} [NeZero m] {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ξ : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun F₀ ι ℓ) (project : QLD.Answer F m d → ι → F₀) (D : (ι → F₀) → (ι → F₀) → A → A → Bool) (S : Ξ.ProjStrat (fullGame hm b L project D)) (a₀ : QLD.Answer F m d) (q : QLD.PauliCL.BinaryQuestion m t) : IsPVMIn (alice hm b L project D S a₀ q).op

theorem MIPRE.Introspection.PauliRestriction.bob_isPVM {F : Type u_1} {F₀ : Type u_2} {ι : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Field F₀] [Fintype F₀] [DecidableEq F₀] [Fintype ι] [DecidableEq ι] [Fintype A] {m t d ℓ : ℕ} [NeZero m] {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ξ : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun F₀ ι ℓ) (project : QLD.Answer F m d → ι → F₀) (D : (ι → F₀) → (ι → F₀) → A → A → Bool) (S : Ξ.ProjStrat (fullGame hm b L project D)) (b₀ : QLD.Answer F m d) (q : QLD.PauliCL.BinaryQuestion m t) : IsPVMIn (bob hm b L project D S b₀ q).op

def MIPRE.Introspection.PauliRestriction.binaryStrategy {F : Type u_1} {F₀ : Type u_2} {ι : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Field F₀] [Fintype F₀] [DecidableEq F₀] [Fintype ι] [DecidableEq ι] [Fintype A] {m t d ℓ : ℕ} [NeZero m] {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ξ : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun F₀ ι ℓ) (project : QLD.Answer F m d → ι → F₀) (D : (ι → F₀) → (ι → F₀) → A → A → Bool) (S : Ξ.ProjStrat (fullGame hm b L project D)) (a₀ b₀ : QLD.Answer F m d) : Ξ.ProjStrat (QLD.PauliCL.binaryGame hm b)

Restriction and answer completion preserve the actual original state.

Equations

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

theorem MIPRE.Introspection.PauliRestriction.binaryStrategy_failAt_le {F : Type u_1} {F₀ : Type u_2} {ι : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Field F₀] [Fintype F₀] [DecidableEq F₀] [Fintype ι] [DecidableEq ι] [Fintype A] {m t d ℓ : ℕ} [NeZero m] {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ξ : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun F₀ ι ℓ) (project : QLD.Answer F m d → ι → F₀) (D : (ι → F₀) → (ι → F₀) → A → A → Bool) (S : Ξ.ProjStrat (fullGame hm b L project D)) (a₀ b₀ : QLD.Answer F m d) (x y : QLD.PauliCL.BinaryQuestion m t) : Ξ.condFail (QLD.PauliCL.binaryGame hm b) (binaryStrategy hm b L project D S a₀ b₀).PA (binaryStrategy hm b L project D S a₀ b₀).PB x y ≤ Ξ.condFail (fullGame hm b L project D) S.PA S.PB (Sum.inl x.1, x.2) (Sum.inl y.1, y.2)

theorem MIPRE.Introspection.PauliRestriction.binaryStrategy_failure_le {F : Type u_1} {F₀ : Type u_2} {ι : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Field F₀] [Fintype F₀] [DecidableEq F₀] [Fintype ι] [DecidableEq ι] [Fintype A] {m t d ℓ : ℕ} [NeZero m] {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ξ : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun F₀ ι ℓ) (project : QLD.Answer F m d → ι → F₀) (D : (ι → F₀) → (ι → F₀) → A → A → Bool) (S : Ξ.ProjStrat (fullGame hm b L project D)) (a₀ b₀ : QLD.Answer F m d) {ε : ℝ} (hS : 1 - S.value ≤ ε) : 1 - (binaryStrategy hm b L project D S a₀ b₀).value ≤ ↑(TypeGraph.edges QLD.adj (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) ℓ).card * ε

The full ordered-edge count is a uniform soundness factor for restriction.

noncomputable def MIPRE.Introspection.PauliRestriction.strategy {F : Type u_1} {F₀ : Type u_2} {ι : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Field F₀] [Fintype F₀] [DecidableEq F₀] [Fintype ι] [DecidableEq ι] [Fintype A] {m t d ℓ : ℕ} [NeZero m] {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ξ : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun F₀ ι ℓ) (project : QLD.Answer F m d → ι → F₀) (D : (ι → F₀) → (ι → F₀) → A → A → Bool) (S : Ξ.ProjStrat (fullGame hm b L project D)) (a₀ b₀ : QLD.Answer F m d) : Ξ.ProjStrat (QLD.qldGame hm)

The actual QLD strategy obtained by canonical question pullback.

Equations

• MIPRE.Introspection.PauliRestriction.strategy hm b L project D S a₀ b₀ = MIPRE.QLD.PauliCL.pullbackStrategy hm b (MIPRE.Introspection.PauliRestriction.binaryStrategy hm b L project D S a₀ b₀)

theorem MIPRE.Introspection.PauliRestriction.strategy_failure_le {F : Type u_1} {F₀ : Type u_2} {ι : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Field F₀] [Fintype F₀] [DecidableEq F₀] [Fintype ι] [DecidableEq ι] [Fintype A] {m t d ℓ : ℕ} [NeZero m] {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ξ : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun F₀ ι ℓ) (project : QLD.Answer F m d → ι → F₀) (D : (ι → F₀) → (ι → F₀) → A → A → Bool) (S : Ξ.ProjStrat (fullGame hm b L project D)) (a₀ b₀ : QLD.Answer F m d) {ε : ℝ} (hS : 1 - S.value ≤ ε) : 1 - (strategy hm b L project D S a₀ b₀).value ≤ ↑(TypeGraph.edges QLD.adj (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) ℓ).card * ε

theorem MIPRE.Introspection.PauliRestriction.strategy_pauli_A {F : Type u_1} {F₀ : Type u_2} {ι : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Field F₀] [Fintype F₀] [DecidableEq F₀] [Fintype ι] [DecidableEq ι] [Fintype A] {m t d ℓ : ℕ} [NeZero m] {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ξ : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun F₀ ι ℓ) (project : QLD.Answer F m d → ι → F₀) (D : (ι → F₀) → (ι → F₀) → A → A → Bool) (S : Ξ.ProjStrat (fullGame hm b L project D)) (a₀ b₀ : QLD.Answer F m d) (W : QLD.Bas) : (strategy hm b L project D S a₀ b₀).PA (QLD.Question.pauli W) = completePauliPOVM a₀ (S.PA (QuestionType.pauli (QLD.Ty.pauli W), 0))

theorem MIPRE.Introspection.PauliRestriction.strategy_pauli_B {F : Type u_1} {F₀ : Type u_2} {ι : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Field F₀] [Fintype F₀] [DecidableEq F₀] [Fintype ι] [DecidableEq ι] [Fintype A] {m t d ℓ : ℕ} [NeZero m] {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ξ : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun F₀ ι ℓ) (project : QLD.Answer F m d → ι → F₀) (D : (ι → F₀) → (ι → F₀) → A → A → Bool) (S : Ξ.ProjStrat (fullGame hm b L project D)) (a₀ b₀ : QLD.Answer F m d) (W : QLD.Bas) : (strategy hm b L project D S a₀ b₀).PB (QLD.Question.pauli W) = completePauliPOVM b₀ (S.PB (QuestionType.pauli (QLD.Ty.pauli W), 0))

theorem MIPRE.Introspection.PauliRestriction.strategy_pauliAns_A {F : Type u_1} {F₀ : Type u_2} {ι : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Field F₀] [Fintype F₀] [DecidableEq F₀] [Fintype ι] [DecidableEq ι] [Fintype A] {m t d ℓ : ℕ} [NeZero m] {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ξ : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun F₀ ι ℓ) (project : QLD.Answer F m d → ι → F₀) (D : (ι → F₀) → (ι → F₀) → A → A → Bool) (S : Ξ.ProjStrat (fullGame hm b L project D)) (W : QLD.Bas) (a : (Fin m → Bool) → F) : ((strategy hm b L project D S (QLD.Answer.val 0) (QLD.Answer.val 0)).PA (QLD.Question.pauli W)).op (QLD.Answer.pauliAns a) = (S.PA (QuestionType.pauli (QLD.Ty.pauli W), 0)).op (ParsedAnswer.pauli (QLD.Answer.pauliAns a))

Choosing a scalar completion answer leaves every genuine Pauli answer operator exactly unchanged, even when malformed outer answers have mass.

theorem MIPRE.Introspection.PauliRestriction.strategy_pauliAns_B {F : Type u_1} {F₀ : Type u_2} {ι : Type u_3} {A : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Field F₀] [Fintype F₀] [DecidableEq F₀] [Fintype ι] [DecidableEq ι] [Fintype A] {m t d ℓ : ℕ} [NeZero m] {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Ξ : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (L : Bool → CL.CLFun F₀ ι ℓ) (project : QLD.Answer F m d → ι → F₀) (D : (ι → F₀) → (ι → F₀) → A → A → Bool) (S : Ξ.ProjStrat (fullGame hm b L project D)) (W : QLD.Bas) (a : (Fin m → Bool) → F) : ((strategy hm b L project D S (QLD.Answer.val 0) (QLD.Answer.val 0)).PB (QLD.Question.pauli W)).op (QLD.Answer.pauliAns a) = (S.PB (QuestionType.pauli (QLD.Ty.pauli W), 0)).op (ParsedAnswer.pauli (QLD.Answer.pauliAns a))