Documentation

MIPRE.Foundations.Introspection.ParsedPauliTransport

Changing only the Pauli payload in a parsed answer #

The map may depend on the question label. Auxiliary registers and source answers are unchanged. Endpoint-local projection agreements suffice for all mixed checks, and equality consistency survives every deterministic map.

source
def MIPRE.Introspection.ParsedAnswer.mapPauli {V : Type u_1} {A : Type u_2} {P : Type u_3} {B : Type u_4} {T : Type u_5} {ℓ : ℕ} (f : QuestionType T ℓ → P → B) (t : QuestionType T ℓ) :
ParsedAnswer V A P → ParsedAnswer V A B
Equations
Instances For
    source
    @[simp]
    theorem MIPRE.Introspection.ParsedAnswer.fits_mapPauli {A : Type u_2} {P : Type u_3} {B : Type u_4} {T : Type u_5} {ℓ : ℕ} {F : Type u_6} {ι : Type u_7} [Field F] [Fintype ι] [DecidableEq ι] (f : QuestionType T ℓ → P → B) (t : QuestionType T ℓ) (a : ParsedAnswer (ι → F) A P) :
    TypedPredicate.fits t (mapPauli f t a) = TypedPredicate.fits t a
    source
    theorem MIPRE.Introspection.AuxiliaryQuotient.directed_mapPauli {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {PB : Type u_5} {P : Type u_6} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : P) (π : PA → ι → F) (π' : PB → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (f : QuestionType P ℓ → PA → PB) (t u : QuestionType P ℓ) (a b : ParsedAnswer (ι → F) A PA) (hp : ∀ (p : P) (c : PA), p = X ∨ p = Z → t = Sum.inl p → a = ParsedAnswer.pauli c → π' (f (Sum.inl p) c) = π c) (h : directed L X Z π D t u a b = true) :
    directed L X Z π' D t u (ParsedAnswer.mapPauli f t a) (ParsedAnswer.mapPauli f u b) = true

    Only the distinguished Pauli endpoints require projection compatibility.

    source
    theorem MIPRE.Introspection.AuxiliaryQuotient.check_mapPauli {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} {PB : Type u_5} {P : Type u_6} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : P) (π : PA → ι → F) (π' : PB → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (f : QuestionType P ℓ → PA → PB) (DP : P → P → PA → PA → Bool) (DP' : P → P → PB → PB → Bool) (t u : QuestionType P ℓ) (a b : ParsedAnswer (ι → F) A PA) (hpa : ∀ (p : P) (c : PA), p = X ∨ p = Z → t = Sum.inl p → a = ParsedAnswer.pauli c → π' (f (Sum.inl p) c) = π c) (hpb : ∀ (p : P) (c : PA), p = X ∨ p = Z → u = Sum.inl p → b = ParsedAnswer.pauli c → π' (f (Sum.inl p) c) = π c) (hDP : ∀ (p q : P) (x y : PA), t = Sum.inl p → u = Sum.inl q → a = ParsedAnswer.pauli x → b = ParsedAnswer.pauli y → DP p q x y = true → DP' p q (f (Sum.inl p) x) (f (Sum.inl q) y) = true) (h : check L X Z π D DP t u a b = true) :
    check L X Z π' D DP' t u (ParsedAnswer.mapPauli f t a) (ParsedAnswer.mapPauli f u b) = true

    A type-dependent Pauli encoding or decoding preserves accepted tuples.

    source
    def MIPRE.Introspection.ParsedAnswer.mapAnswer {V : Type u_1} {A : Type u_2} {B : Type u_3} {PA : Type u_4} (g : A → B) :
    ParsedAnswer V A PA → ParsedAnswer V B PA

    Map the original answer in the pair and Read formats.

    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.Introspection.ParsedAnswer.fits_mapAnswer {A : Type u_2} {B : Type u_3} {PA : Type u_4} {P : Type u_5} {ℓ : ℕ} {F : Type u_6} {ι : Type u_7} [Field F] [Fintype ι] [DecidableEq ι] (g : A → B) (t : QuestionType P ℓ) (a : ParsedAnswer (ι → F) A PA) :
      TypedPredicate.fits t (mapAnswer g a) = TypedPredicate.fits t a
      source
      theorem MIPRE.Introspection.AuxiliaryQuotient.directed_mapAnswer {F : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} {PA : Type u_5} {P : Type u_6} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : P) (π : PA → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (D' : (ι → F) → (ι → F) → B → B → Bool) (g : A → B) (t u : QuestionType P ℓ) (a b : ParsedAnswer (ι → F) A PA) (hD : ∀ (x y : ι → F) (c d : A), a = ParsedAnswer.pair x c → b = ParsedAnswer.pair y d → D x y c d = true → D' x y (g c) (g d) = true) (h : directed L X Z π D t u a b = true) :
      directed L X Z π D' t u (ParsedAnswer.mapAnswer g a) (ParsedAnswer.mapAnswer g b) = true

      Source-predicate compatibility is required only for the actual endpoint payloads.

      source
      theorem MIPRE.Introspection.AuxiliaryQuotient.check_mapAnswer {F : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} {PA : Type u_5} {P : Type u_6} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : P) (π : PA → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (D' : (ι → F) → (ι → F) → B → B → Bool) (g : A → B) (DP : P → P → PA → PA → Bool) (t u : QuestionType P ℓ) (a b : ParsedAnswer (ι → F) A PA) (hD : ∀ (x y : ι → F) (c d : A), a = ParsedAnswer.pair x c → b = ParsedAnswer.pair y d → D x y c d = true → D' x y (g c) (g d) = true) (hDr : ∀ (x y : ι → F) (c d : A), b = ParsedAnswer.pair x c → a = ParsedAnswer.pair y d → D x y c d = true → D' x y (g c) (g d) = true) (h : check L X Z π D DP t u a b = true) :
      check L X Z π D' DP t u (ParsedAnswer.mapAnswer g a) (ParsedAnswer.mapAnswer g b) = true

      In particular, bounded decoding of source answers preserves all accepted checks.