Finite-game transport for quotient hiding checks #
The question law is unchanged. Decoding dual answer coordinates gives a legacy strategy with at least the original value, on the same registers and state and with every Pauli-question effect unchanged. In the other direction, copying a legacy strategy preserves perfect PCC completeness and its dimension.
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 by its type, and the statements about its state and
dimensions have no counterpart. The value comparison quantumValue_eq is the tensor-product
instance.
noncomputable def
MIPRE.Introspection.AuxiliaryQuotient.questionCheck
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{κ : Type u_4}
{A : Type u_5}
[Field F]
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(X Z : PauliType)
(L : Bool → CL.CLFun F ι ℓ)
(project : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
(q r : CL.Detyping.Question (QuestionType PauliType ℓ) κ)
:
ParsedAnswer (ι → F) A PauliAnswer → ParsedAnswer (ι → F) A PauliAnswer → Bool
The complete quotient predicate at actual raw typed questions.
Equations
- MIPRE.Introspection.AuxiliaryQuotient.questionCheck X Z L project D DP q r = MIPRE.Introspection.AuxiliaryQuotient.check L X Z project D (fun (p s : PauliType) => DP p s q.2 r.2) q.1 r.1
Instances For
noncomputable def
MIPRE.Introspection.AuxiliaryQuotient.game
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{κ : Type u_4}
{A : Type u_5}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(P : PauliType → CL.CLFun (ZMod 2) κ 3)
(L : Bool → CL.CLFun F ι ℓ)
(project : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
:
Game (CL.Detyping.Question (QuestionType PauliType ℓ) κ) (CL.Detyping.Question (QuestionType PauliType ℓ) κ)
(ParsedAnswer (ι → F) A PauliAnswer) (ParsedAnswer (ι → F) A PauliAnswer)
The quotient game retains the full legacy question-pair law.
Equations
- MIPRE.Introspection.AuxiliaryQuotient.game E X Z P L project D DP = MIPRE.Introspection.TypedPresentation.game E X Z ℓ P (MIPRE.Introspection.AuxiliaryQuotient.questionCheck X Z L project D DP)
Instances For
theorem
MIPRE.Introspection.AuxiliaryQuotient.game_accepts_of_legacy
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{κ : Type u_4}
{A : Type u_5}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(P : PauliType → CL.CLFun (ZMod 2) κ 3)
(L : Bool → CL.CLFun F ι ℓ)
(project : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
(hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ)
(q r : CL.Detyping.Question (QuestionType PauliType ℓ) κ)
(a b : ParsedAnswer (ι → F) A PauliAnswer)
(h : (TypedEstimates.parsedGame E X Z P L project D DP).D q r a b = true)
:
Legacy acceptance implies quotient acceptance on every raw tuple.
@[reducible, inline]
noncomputable abbrev
MIPRE.Introspection.AuxiliaryQuotient.decodedStrategy
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{κ : Type u_4}
{A : Type u_5}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(P : PauliType → CL.CLFun (ZMod 2) κ 3)
(L : Bool → CL.CLFun F ι ℓ)
(project : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
{Ψ : BipartiteModel 𝒞 𝒜 ℬ}
(S : Ψ.ProjStrat (game E X Z P L project D DP))
:
Ψ.ProjStrat (TypedEstimates.parsedGame E X Z P L project D DP)
Decode auxiliary answers according to their question's side.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPRE.Introspection.AuxiliaryQuotient.value_le_decodedStrategy
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{κ : Type u_4}
{A : Type u_5}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(P : PauliType → CL.CLFun (ZMod 2) κ 3)
(L : Bool → CL.CLFun F ι ℓ)
(project : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
{Ψ : BipartiteModel 𝒞 𝒜 ℬ}
(hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ)
(S : Ψ.ProjStrat (game E X Z P L project D DP))
:
Deterministic answer decoding does not decrease the winning probability.
theorem
MIPRE.Introspection.AuxiliaryQuotient.decodedStrategy_failure_le
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{κ : Type u_4}
{A : Type u_5}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(P : PauliType → CL.CLFun (ZMod 2) κ 3)
(L : Bool → CL.CLFun F ι ℓ)
(project : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
{Ψ : BipartiteModel 𝒞 𝒜 ℬ}
(hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ)
(S : Ψ.ProjStrat (game E X Z P L project D DP))
{ε : ℝ}
(hS : 1 - S.value ≤ ε)
:
Any failure bound for the quotient strategy also bounds its legacy decoding.
theorem
MIPRE.Introspection.AuxiliaryQuotient.decodedStrategy_pauli_A
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{κ : Type u_4}
{A : Type u_5}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(P : PauliType → CL.CLFun (ZMod 2) κ 3)
(L : Bool → CL.CLFun F ι ℓ)
(project : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
{Ψ : BipartiteModel 𝒞 𝒜 ℬ}
(S : Ψ.ProjStrat (game E X Z P L project D DP))
(p : PauliType)
(x : κ → ZMod 2)
(a : ParsedAnswer (ι → F) A PauliAnswer)
:
Every Alice effect at every Pauli question is unchanged.
theorem
MIPRE.Introspection.AuxiliaryQuotient.decodedStrategy_pauli_B
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{κ : Type u_4}
{A : Type u_5}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(P : PauliType → CL.CLFun (ZMod 2) κ 3)
(L : Bool → CL.CLFun F ι ℓ)
(project : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
{Ψ : BipartiteModel 𝒞 𝒜 ℬ}
(S : Ψ.ProjStrat (game E X Z P L project D DP))
(p : PauliType)
(x : κ → ZMod 2)
(a : ParsedAnswer (ι → F) A PauliAnswer)
:
Every Bob effect at every Pauli question is unchanged.
@[reducible, inline]
noncomputable abbrev
MIPRE.Introspection.AuxiliaryQuotient.copiedPCC
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{κ : Type u_4}
{A : Type u_5}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(P : PauliType → CL.CLFun (ZMod 2) κ 3)
(L : Bool → CL.CLFun F ι ℓ)
(project : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
[DecidableEq A]
[DecidableEq PauliAnswer]
(S : SyncStrategy (TypedEstimates.parsedGame E X Z P L project D DP).doubled)
:
SyncStrategy (game E X Z P L project D DP).doubled
Copy the honest synchronous data to the doubled quotient game.
Equations
- MIPRE.Introspection.AuxiliaryQuotient.copiedPCC E X Z P L project D DP S = S.copy (MIPRE.Introspection.AuxiliaryQuotient.game E X Z P L project D DP).doubled
Instances For
theorem
MIPRE.Introspection.AuxiliaryQuotient.copiedPCC_isPCC
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{κ : Type u_4}
{A : Type u_5}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(P : PauliType → CL.CLFun (ZMod 2) κ 3)
(L : Bool → CL.CLFun F ι ℓ)
(project : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
[DecidableEq A]
[DecidableEq PauliAnswer]
(S : SyncStrategy (TypedEstimates.parsedGame E X Z P L project D DP).doubled)
(hS : S.IsPCC)
:
Copying an honest strategy keeps its PCC property.
theorem
MIPRE.Introspection.AuxiliaryQuotient.copiedPCC_value_eq_one
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{κ : Type u_4}
{A : Type u_5}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(P : PauliType → CL.CLFun (ZMod 2) κ 3)
(L : Bool → CL.CLFun F ι ℓ)
(project : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
[DecidableEq A]
[DecidableEq PauliAnswer]
(hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ)
(S : SyncStrategy (TypedEstimates.parsedGame E X Z P L project D DP).doubled)
(hS : S.value = 1)
:
Every perfect legacy PCC strategy remains perfect in the quotient game.