Quotient hiding checks commute with coordinate permutations #
Only equality of dual quotient classes is transported. The chosen canonical representatives themselves need not commute with a permutation.
theorem
MIPRE.Introspection.AuxiliaryQuotient.reindex_eq_iff
{F : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Field F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
(e : ι ≃ κ)
(x y : ι → F)
:
theorem
MIPRE.Introspection.AuxiliaryQuotient.dot_reindex
{F : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Field F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
(e : ι ≃ κ)
(x y : ι → F)
:
theorem
MIPRE.Introspection.AuxiliaryQuotient.stageDual_reindex_eq_iff
{F : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Field F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
{ℓ : ℕ}
(e : ι ≃ κ)
(P : CL.CLFun F ι ℓ)
(k : ℕ)
(y x z : ι → F)
:
(AuxiliaryDual.stageDual (CL.CLFun.reindex e P) k ((CL.reindexEquiv e) y)) ((CL.reindexEquiv e) x) = (AuxiliaryDual.stageDual (CL.CLFun.reindex e P) k ((CL.reindexEquiv e) y)) ((CL.reindexEquiv e) z) ↔ (AuxiliaryDual.stageDual P k y) x = (AuxiliaryDual.stageDual P k y) z
Equality of stage-dual outputs is intrinsic, despite their chosen labels.
def
MIPRE.Introspection.AuxiliaryQuotient.answerEquiv
{F : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
{A : Type u_4}
{PA : Type u_5}
[Field F]
(e : ι ≃ κ)
:
Relabel all binary-register components, retaining ordinary and Pauli answers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
MIPRE.Introspection.AuxiliaryQuotient.fits_answerEquiv
{F : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
{A : Type u_4}
{PA : Type u_5}
{PT : Type u_6}
[Field F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
{ℓ : ℕ}
(e : ι ≃ κ)
(t : QuestionType PT ℓ)
(a : ParsedAnswer (ι → F) A PA)
:
theorem
MIPRE.Introspection.AuxiliaryQuotient.hidingNext_reindex
{F : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Field F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
{ℓ : ℕ}
(e : ι ≃ κ)
(P : CL.CLFun F ι ℓ)
(k : ℕ)
(y yp x z zp v : ι → F)
:
hidingNext (CL.CLFun.reindex e P) k ((CL.reindexEquiv e) y, (CL.reindexEquiv e) yp, (CL.reindexEquiv e) x)
((CL.reindexEquiv e) z, (CL.reindexEquiv e) zp, (CL.reindexEquiv e) v) ↔ hidingNext P k (y, yp, x) (z, zp, v)
theorem
MIPRE.Introspection.AuxiliaryQuotient.hidingPauli_reindex
{F : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Field F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
{ℓ : ℕ}
(e : ι ≃ κ)
(P : CL.CLFun F ι ℓ)
(x y yp z : ι → F)
:
hidingPauli (CL.CLFun.reindex e P) ((CL.reindexEquiv e) x)
((CL.reindexEquiv e) y, (CL.reindexEquiv e) yp, (CL.reindexEquiv e) z) ↔ hidingPauli P x (y, yp, z)
theorem
MIPRE.Introspection.AuxiliaryQuotient.hidingRead_reindex
{F : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
{A : Type u_4}
[Field F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
{ℓ : ℕ}
(e : ι ≃ κ)
(P : CL.CLFun F ι ℓ)
(y yp x z zp : ι → F)
(a : A)
:
CLChecks.hidingRead (CL.CLFun.reindex e P) ((CL.reindexEquiv e) y, (CL.reindexEquiv e) yp, (CL.reindexEquiv e) x)
((CL.reindexEquiv e) z, (CL.reindexEquiv e) zp, a) ↔ CLChecks.hidingRead P (y, yp, x) (z, zp, a)
theorem
MIPRE.Introspection.AuxiliaryQuotient.directed_reindex
{F : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
{A : Type u_4}
{PA : Type u_5}
{PT : Type u_6}
[Field F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
{ℓ : ℕ}
(e : ι ≃ κ)
(L : Bool → CL.CLFun F ι ℓ)
(X Z : PT)
(project : PA → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(t u : QuestionType PT ℓ)
(a b : ParsedAnswer (ι → F) A PA)
:
directed (fun (w : Bool) => CL.CLFun.reindex e (L w)) X Z (fun (a : PA) => (CL.reindexEquiv e) (project a))
(fun (x y : κ → F) => D ((CL.reindexEquiv e).symm x) ((CL.reindexEquiv e).symm y)) t u ((answerEquiv e) a)
((answerEquiv e) b) = directed L X Z project D t u a b
theorem
MIPRE.Introspection.AuxiliaryQuotient.check_reindex
{F : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
{A : Type u_4}
{PA : Type u_5}
{PT : Type u_6}
[Field F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
{ℓ : ℕ}
(e : ι ≃ κ)
(L : Bool → CL.CLFun F ι ℓ)
(X Z : PT)
(project : PA → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PT → PT → PA → PA → Bool)
(t u : QuestionType PT ℓ)
(a b : ParsedAnswer (ι → F) A PA)
:
check (fun (w : Bool) => CL.CLFun.reindex e (L w)) X Z (fun (a : PA) => (CL.reindexEquiv e) (project a))
(fun (x y : κ → F) => D ((CL.reindexEquiv e).symm x) ((CL.reindexEquiv e).symm y)) DP t u ((answerEquiv e) a)
((answerEquiv e) b) = check L X Z project D DP t u a b