Exact strategy transport between the Pauli game and its binary CL form

Question content has a canonical ambient encoding, with unused registers set to zero. This encoding inverts the decoder on every attained CL output. Consequently arbitrary strategies for the binary typed game pull back to the existing Pauli game with exactly the same state, dimensions, and value.

The strategies are projective strategies of any bipartite model (Phase 4 of planning/mipco-track.md); the pullback stays in the same model.

def MIPRE.QLD.PauliCL.pointContent {F : Type u_1} [Field F] {m : ℕ} (W : Bas) (u : Fin m → F) (s : F) (v : Fin m → F) : Content F m

Equations

• MIPRE.QLD.PauliCL.pointContent MIPRE.QLD.Bas.X u s v = { uX := u, uZ := 0, s := s, v := v, rX := 0, rZ := 0 }
• MIPRE.QLD.PauliCL.pointContent MIPRE.QLD.Bas.Z u s v = { uX := 0, uZ := u, s := s, v := v, rX := 0, rZ := 0 }

def MIPRE.QLD.PauliCL.omegaContent {F : Type u_1} [Field F] {m : ℕ} (ω : Omega F m) : Content F m

Equations

• MIPRE.QLD.PauliCL.omegaContent ω = { uX := ω.uX, uZ := ω.uZ, s := 0, v := 0, rX := ω.rX, rZ := ω.rZ }

def MIPRE.QLD.PauliCL.canonicalVector {F : Type u_1} [Field F] {m : ℕ} (q : Question F m) : Coord m → F

The canonical ambient encoding of question content.

Equations

• MIPRE.QLD.PauliCL.canonicalVector (MIPRE.QLD.Question.point W u) = MIPRE.QLD.PauliCL.contentVector (MIPRE.QLD.PauliCL.pointContent W u 0 0)
• MIPRE.QLD.PauliCL.canonicalVector (MIPRE.QLD.Question.aline W u s) = MIPRE.QLD.PauliCL.contentVector (MIPRE.QLD.PauliCL.pointContent W u s 0)
• MIPRE.QLD.PauliCL.canonicalVector (MIPRE.QLD.Question.dline W u s v) = MIPRE.QLD.PauliCL.contentVector (MIPRE.QLD.PauliCL.pointContent W u s v)
• MIPRE.QLD.PauliCL.canonicalVector (MIPRE.QLD.Question.pauli W) = MIPRE.QLD.PauliCL.contentVector { uX := 0, uZ := 0, s := 0, v := 0, rX := 0, rZ := 0 }
• MIPRE.QLD.PauliCL.canonicalVector (MIPRE.QLD.Question.pairB W ω) = MIPRE.QLD.PauliCL.contentVector (MIPRE.QLD.PauliCL.omegaContent ω)
• MIPRE.QLD.PauliCL.canonicalVector (MIPRE.QLD.Question.pair ω) = MIPRE.QLD.PauliCL.contentVector (MIPRE.QLD.PauliCL.omegaContent ω)
• MIPRE.QLD.PauliCL.canonicalVector (MIPRE.QLD.Question.con i ω) = MIPRE.QLD.PauliCL.contentVector (MIPRE.QLD.PauliCL.omegaContent ω)
• MIPRE.QLD.PauliCL.canonicalVector (MIPRE.QLD.Question.var j ω) = MIPRE.QLD.PauliCL.contentVector (MIPRE.QLD.PauliCL.omegaContent ω)

theorem MIPRE.QLD.PauliCL.canonicalVector_pauli {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (W : Bas) : canonicalVector (Question.pauli W) = 0

theorem MIPRE.QLD.PauliCL.questionOfVector_canonical {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] (q : Question F m) : questionOfVector q.ty (canonicalVector q) = q

theorem MIPRE.QLD.PauliCL.canonicalVector_question {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (T : Ty) (c : Content F m) : canonicalVector (Content.question hm c T) = (presentation hm T).eval (contentVector c)

No information is lost by decoding an attained field CL output.

@[reducible, inline]

abbrev MIPRE.QLD.PauliCL.BinaryQuestion (m t : ℕ) : Type

Equations

• MIPRE.QLD.PauliCL.BinaryQuestion m t = (MIPRE.QLD.Ty × (Fin ((3 * m + 3) * t) → ZMod 2))

noncomputable def MIPRE.QLD.PauliCL.encodeQuestion {F : Type u_1} [Field F] {m : ℕ} [Algebra (ZMod 2) F] {t : ℕ} (b : Module.Basis (Fin t) (ZMod 2) F) (q : Question F m) : BinaryQuestion m t

Equations

• MIPRE.QLD.PauliCL.encodeQuestion b q = (q.ty, (MIPRE.QLD.PauliCL.binaryVectorEquiv b) (MIPRE.QLD.PauliCL.canonicalVector q))

noncomputable def MIPRE.QLD.PauliCL.decodeQuestion {F : Type u_1} [Field F] {m : ℕ} [Algebra (ZMod 2) F] {t : ℕ} (b : Module.Basis (Fin t) (ZMod 2) F) (q : BinaryQuestion m t) : Question F m

Equations

• MIPRE.QLD.PauliCL.decodeQuestion b q = MIPRE.QLD.PauliCL.binaryQuestion b q.1 q.2

theorem MIPRE.QLD.PauliCL.encodeQuestion_seed {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [Algebra (ZMod 2) F] [NeZero m] {t : ℕ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (T : Ty) (c : Content F m) : encodeQuestion b (Content.question hm c T) = (T, (binaryPresentation hm b T).eval ((binaryVectorEquiv b) (contentVector c)))

theorem MIPRE.QLD.PauliCL.encode_decode_eval {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [Algebra (ZMod 2) F] [NeZero m] {t : ℕ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (T : Ty) (x : Fin ((3 * m + 3) * t) → ZMod 2) : encodeQuestion b (decodeQuestion b (T, (binaryPresentation hm b T).eval x)) = (T, (binaryPresentation hm b T).eval x)

The inverse law is restricted to actual CL outputs, as required.

noncomputable def MIPRE.QLD.PauliCL.binaryQuery {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [Algebra (ZMod 2) F] [NeZero m] {t : ℕ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (w : Bool) (p : TyEdge × (Fin ((3 * m + 3) * t) → ZMod 2)) : BinaryQuestion m t

Equations

• MIPRE.QLD.PauliCL.binaryQuery hm b w p = (if w = true then (↑p.1).2 else (↑p.1).1, (MIPRE.QLD.PauliCL.binaryPresentation hm b (if w = true then (↑p.1).2 else (↑p.1).1)).eval p.2)

noncomputable def MIPRE.QLD.PauliCL.binaryGame {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [Algebra (ZMod 2) F] [NeZero m] {t d : ℕ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) : Game (BinaryQuestion m t) (BinaryQuestion m t) (Answer F m d) (Answer F m d)

The actual typed binary CL game, with the existing Pauli acceptance rule applied to decoded questions.

Equations

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

noncomputable def MIPRE.QLD.PauliCL.pullbackStrategy {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [Algebra (ZMod 2) F] [NeZero m] {t d : ℕ} {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (S : M.ProjStrat (binaryGame hm b)) : M.ProjStrat (qldGame hm)

Play the binary game's measurements at the canonical encoding of each Pauli question. The model, and so the shared state, is unchanged.

Equations

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

theorem MIPRE.QLD.PauliCL.pullbackStrategy_value {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [Algebra (ZMod 2) F] [NeZero m] {t d : ℕ} {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (S : M.ProjStrat (binaryGame hm b)) : (pullbackStrategy hm b S).value = S.value

theorem MIPRE.QLD.PauliCL.pullbackStrategy_pauli_A {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [Algebra (ZMod 2) F] [NeZero m] {t d : ℕ} {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (S : M.ProjStrat (binaryGame hm b)) (W : Bas) : (pullbackStrategy hm b S).PA (Question.pauli W) = S.PA (Ty.pauli W, 0)

theorem MIPRE.QLD.PauliCL.pullbackStrategy_pauli_B {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [Algebra (ZMod 2) F] [NeZero m] {t d : ℕ} {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (S : M.ProjStrat (binaryGame hm b)) (W : Bas) : (pullbackStrategy hm b S).PB (Question.pauli W) = S.PB (Ty.pauli W, 0)