Full typed introspection under an explicit Pauli seed enumeration

The equivalence acts on all raw questions, preserves the type, and fixes the auxiliary questions and both distinguished Pauli measurements. A permutation of the common random content proves equality of the full question-pair law, including mixed Pauli/auxiliary edges. The parsed predicate is intertwined on every question and every answer, including malformed answers and loops.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the soundness transports toLegacy relabels a projective strategy of one model M along the question equivalence (BipartiteModel.ProjStrat.relabel), so the transported strategy lives in the same model and the state is unchanged by construction. The Pauli lemmas are equalities of POVMs. The completeness transports (pccToExplicit*) stay on synchronous matrix strategies.

@[reducible, inline]

abbrev MIPRE.Introspection.ExplicitGame.Question (m t ℓ : ℕ) : Type

Raw questions consist of an introspection type and its full binary content.

Equations

• MIPRE.Introspection.ExplicitGame.Question m t ℓ = MIPRE.CL.Detyping.Question (MIPRE.Introspection.QuestionType MIPRE.QLD.Ty ℓ) (Fin ((3 * m + 3) * t))

noncomputable def MIPRE.Introspection.ExplicitGame.contentPermutation {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m t ℓ : ℕ} (π : F ≃ F) (b : Module.Basis (Fin t) (ZMod 2) F) : QuestionType QLD.Ty ℓ → (Fin ((3 * m + 3) * t) → ZMod 2) ≃ (Fin ((3 * m + 3) * t) → ZMod 2)

Change only the Pauli contents whose decoding retains the seed.

Equations

• MIPRE.Introspection.ExplicitGame.contentPermutation π b (Sum.inl p) = MIPRE.QLD.PauliCL.ExplicitSeed.binaryOutputPermutation π b p
• MIPRE.Introspection.ExplicitGame.contentPermutation π b (Sum.inr val) = Equiv.refl (Fin ((3 * m + 3) * t) → ZMod 2)

noncomputable def MIPRE.Introspection.ExplicitGame.questionEquiv {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {m t ℓ : ℕ} (π : F ≃ F) (b : Module.Basis (Fin t) (ZMod 2) F) : Question m t ℓ ≃ Question m t ℓ

A total equivalence of full raw typed questions, not only sampled outputs.

Equations

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

@[simp]

theorem MIPRE.Introspection.ExplicitGame.questionEquiv_aux {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t ℓ : ℕ} [NeZero m] (π : F ≃ F) (b : Module.Basis (Fin t) (ZMod 2) F) (u : AuxType ℓ) (w : Bool) (x : Fin ((3 * m + 3) * t) → ZMod 2) : (questionEquiv π b) (Sum.inr (u, w), x) = (Sum.inr (u, w), x)

The question equivalence fixes every auxiliary question.

@[simp]

theorem MIPRE.Introspection.ExplicitGame.questionEquiv_pauli {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t ℓ : ℕ} [NeZero m] (π : F ≃ F) (b : Module.Basis (Fin t) (ZMod 2) F) (W : QLD.Bas) (x : Fin ((3 * m + 3) * t) → ZMod 2) : (questionEquiv π b) (Sum.inl (QLD.Ty.pauli W), x) = (Sum.inl (QLD.Ty.pauli W), x)

The question equivalence fixes both distinguished Pauli questions.

@[simp]

theorem MIPRE.Introspection.ExplicitGame.questionEquiv_symm_pauli {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t ℓ : ℕ} [NeZero m] (π : F ≃ F) (b : Module.Basis (Fin t) (ZMod 2) F) (W : QLD.Bas) (x : Fin ((3 * m + 3) * t) → ZMod 2) : (questionEquiv π b).symm (Sum.inl (QLD.Ty.pauli W), x) = (Sum.inl (QLD.Ty.pauli W), x)

The inverse equivalence also fixes both distinguished Pauli questions.

noncomputable def MIPRE.Introspection.ExplicitGame.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) (π : F ≃ 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

The Pauli decision predicate with the explicit seed decoder.

Equations

• MIPRE.Introspection.ExplicitGame.pauliCheck hm π b p q x y = MIPRE.QLD.accepts hm (MIPRE.QLD.PauliCL.ExplicitSeed.binaryDecode π b p x) (MIPRE.QLD.PauliCL.ExplicitSeed.binaryDecode π b q y)

noncomputable def MIPRE.Introspection.ExplicitGame.game {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) (χ : F → Fin m) (π : F ≃ 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 (Question m t ℓ) (Question m t ℓ) (ParsedAnswer (ι → F₀) A (QLD.Answer F m d)) (ParsedAnswer (ι → F₀) A (QLD.Answer F m d))

The actual explicit-selector typed game, with the same source predicate.

Equations

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

theorem MIPRE.Introspection.ExplicitGame.questionEquiv_family {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m t ℓ : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ F) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) (b : Module.Basis (Fin t) (ZMod 2) F) (u : QuestionType QLD.Ty ℓ) (x : Fin ((3 * m + 3) * t) → ZMod 2) : (questionEquiv π b) (u, (TypedPresentation.family (QLD.PauliCL.ExplicitSeed.binaryPresentation χ b) u).eval x) = (u, (TypedPresentation.family (QLD.PauliCL.binaryPresentation hm b) u).eval ((QLD.PauliCL.ExplicitSeed.binarySeedPermutation π b) x))

The raw question equivalence intertwines every sampled typed question.

theorem MIPRE.Introspection.ExplicitGame.dist_equiv {S : Type u_5} {X : Type u_6} [Fintype S] [Fintype X] (a b c d : S → X) (e : S ≃ S) (f : X ≃ X) (ha : ∀ (s : S), f (a s) = c (e s)) (hb : ∀ (s : S), f (b s) = d (e s)) (x y : X) : SampledGame.dist a b x y = SampledGame.dist c d (f x) (f y)

Simultaneous seed and output equivalences preserve the joint sampling law.

theorem MIPRE.Introspection.ExplicitGame.game_mu {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] (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ F) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) (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) (q r : Question m t ℓ) : (game hm χ π b L project D).μ q r = (PauliRestriction.fullGame hm b L project D).μ ((questionEquiv π b) q) ((questionEquiv π b) r)

Equality of the complete typed law, including every auxiliary and mixed edge.

theorem MIPRE.Introspection.ExplicitGame.game_D {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] (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ 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) (q r : Question m t ℓ) (a a' : ParsedAnswer (ι → F₀) A (QLD.Answer F m d)) : (game hm χ π b L project D).D q r a a' = (PauliRestriction.fullGame hm b L project D).D ((questionEquiv π b) q) ((questionEquiv π b) r) a a'

Exact decision equality on all raw questions and all parsed answers.

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.ExplicitGame.toLegacy {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] (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ 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) {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (game hm χ π b L project D)) : M.ProjStrat (PauliRestriction.fullGame hm b L project D)

Transport an explicit strategy back to the legacy full game, in the same model.

Equations

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

theorem MIPRE.Introspection.ExplicitGame.toLegacy_value {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] (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ F) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) (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) {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (game hm χ π b L project D)) : (toLegacy hm χ π b L project D S).value = S.value

Transport to the legacy game preserves the strategy value.

theorem MIPRE.Introspection.ExplicitGame.toLegacy_eq_restrict {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] (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ 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) {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (game hm χ π b L project D)) : toLegacy hm χ π b L project D S = S.restrict (PauliRestriction.fullGame hm b L project D) ⇑(questionEquiv π b).symm ⇑(questionEquiv π b).symm

The legacy transport keeps every measurement: relabelling along the identity of the answers is the restriction to the relabelled questions (POVMIn.map_id).

theorem MIPRE.Introspection.ExplicitGame.toLegacy_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] (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ 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) {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (game hm χ π b L project D)) (W : QLD.Bas) : (toLegacy hm χ π b L project D S).PA (Sum.inl (QLD.Ty.pauli W), 0) = S.PA (Sum.inl (QLD.Ty.pauli W), 0)

Legacy transport preserves Alice's distinguished Pauli measurements.

theorem MIPRE.Introspection.ExplicitGame.toLegacy_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] (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ 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) {𝒞 : Type u_5} {𝒜 : Type u_6} {ℬ : Type u_7} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (game hm χ π b L project D)) (W : QLD.Bas) : (toLegacy hm χ π b L project D S).PB (Sum.inl (QLD.Ty.pauli W), 0) = S.PB (Sum.inl (QLD.Ty.pauli W), 0)

Legacy transport preserves Bob's distinguished Pauli measurements.

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.ExplicitGame.pccToExplicit {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] (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ 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) [DecidableEq A] (S : SyncStrategy (PauliRestriction.fullGame hm b L project D).doubled) : SyncStrategy (game hm χ π b L project D).doubled

The same relabeling on the doubled questions used by PCC completeness.

Equations

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

theorem MIPRE.Introspection.ExplicitGame.pccToExplicit_isPCC {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] (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ F) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) (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) [DecidableEq A] (S : SyncStrategy (PauliRestriction.fullGame hm b L project D).doubled) (hS : S.IsPCC) : (pccToExplicit hm χ π b L project D S).IsPCC

Relabeling the doubled game preserves the PCC property.

theorem MIPRE.Introspection.ExplicitGame.pccToExplicit_value {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] (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ F) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) (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) [DecidableEq A] (S : SyncStrategy (PauliRestriction.fullGame hm b L project D).doubled) : (pccToExplicit hm χ π b L project D S).value = S.value

Relabeling the doubled game preserves the strategy value.