Documentation

MIPRE.Foundations.Introspection.TypedPresentation

The typed introspection CL presentation #

The three-level Pauli presentations are retained verbatim. Every auxiliary type uses the zero presentation, padded to three levels with a full factor partition. Both players use the same family. The corresponding finite game has an exactly uniform ordered-edge law, and the cross-introspection edge asks the two zero-content questions with probability the inverse edge count.

source
def MIPRE.Introspection.TypedPresentation.family {PauliType : Type u_1} {F : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Semiring F] {ℓ : ℕ} (P : PauliType → CL.CLFun F ι 3) :
QuestionType PauliType ℓ → CL.CLFun F ι 3

The typed sampler's complete three-level CL family.

Equations
Instances For
    source
    theorem MIPRE.Introspection.TypedPresentation.family_exactlyOn {PauliType : Type u_1} {F : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Semiring F] {ℓ : ℕ} (P : PauliType → CL.CLFun F ι 3) (hP : ∀ (p : PauliType), (P p).ExactlyOn Finset.univ) (t : QuestionType PauliType ℓ) :
    (family P t).ExactlyOn Finset.univ

    The auxiliary zero presentation still partitions the full register.

    source
    @[simp]
    theorem MIPRE.Introspection.TypedPresentation.eval_aux {PauliType : Type u_1} {F : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Semiring F] {ℓ : ℕ} (P : PauliType → CL.CLFun F ι 3) (t : AuxType ℓ) (w : Bool) (z : ι → F) :
    (family P (Sum.inr (t, w))).eval z = 0

    All auxiliary questions have zero content.

    source
    theorem MIPRE.Introspection.TypedPresentation.marginal_aux {PauliType : Type u_1} {F : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Semiring F] {ℓ : ℕ} (P : PauliType → CL.CLFun F ι 3) (t : AuxType ℓ) (w : Bool) (j : ℕ) (z : ι → F) :
    (CL.CLFun.truncate j (family P (Sum.inr (t, w)))).eval z = 0

    The zero-content assertion holds at every truncation level.

    source
    theorem MIPRE.Introspection.TypedPresentation.linear_aux {PauliType : Type u_1} {F : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Semiring F] {ℓ : ℕ} (P : PauliType → CL.CLFun F ι 3) (t : AuxType ℓ) (w : Bool) (j : ℕ) (u : ι → F) :
    (family P (Sum.inr (t, w))).mapOfPrefix j u = 0

    Every linear query for an auxiliary question is the zero map.

    source
    theorem MIPRE.Introspection.TypedPresentation.factor_aux {PauliType : Type u_1} {F : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Semiring F] {ℓ : ℕ} (P : PauliType → CL.CLFun F ι 3) (t : AuxType ℓ) (w : Bool) (j : ℕ) (u : ι → F) :
    (family P (Sum.inr (t, w))).factorOfPrefix j u = if j = 0 then Finset.univ else ∅

    The first auxiliary factor consumes the register; later factors are empty.

    source
    theorem MIPRE.Introspection.TypedPresentation.joint_aux_zero {PauliType : Type u_1} {F : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Semiring F] {ℓ : ℕ} (P : PauliType → CL.CLFun F ι 3) (t u : AuxType ℓ) (w w' : Bool) (z : ι → F) :
    ((family P (Sum.inr (t, w))).eval z, (family P (Sum.inr (u, w'))).eval z) = (0, 0)

    Auxiliary questions jointly have zero content even though their seed is shared.

    source
    noncomputable def MIPRE.Introspection.TypedPresentation.game {PauliType : Type u_1} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype PauliType] [DecidableEq PauliType] {A : Type u_4} {B : Type u_5} [Fintype A] [Fintype B] (E : PauliType → PauliType → Bool) (X Z : PauliType) (ℓ : ℕ) (P : PauliType → CL.CLFun (ZMod 2) ι 3) (D : CL.Detyping.Question (QuestionType PauliType ℓ) ι → CL.Detyping.Question (QuestionType PauliType ℓ) ι → A → B → Bool) :
    Game (CL.Detyping.Question (QuestionType PauliType ℓ) ι) (CL.Detyping.Question (QuestionType PauliType ℓ) ι) A B

    The actual finite typed introspection game, for the supplied decision predicate.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.Introspection.TypedPresentation.mu_aux {PauliType : Type u_1} {ι : Type u_3} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype PauliType] [DecidableEq PauliType] {A : Type u_4} {B : Type u_5} [Fintype A] [Fintype B] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) ι 3) (D : CL.Detyping.Question (QuestionType PauliType ℓ) ι → CL.Detyping.Question (QuestionType PauliType ℓ) ι → A → B → Bool) (t u : AuxType ℓ) (w w' : Bool) (h : TypeGraph.Adj E X Z (Sum.inr (t, w)) (Sum.inr (u, w'))) :
      (game E X Z ℓ P D).μ (Sum.inr (t, w), 0) (Sum.inr (u, w'), 0) = (↑(TypeGraph.edges E X Z ℓ).card)⁻¹

      A fixed edge between auxiliary types has exactly inverse-edge-count probability.

      source
      theorem MIPRE.Introspection.TypedPresentation.mu_cross_introspect {PauliType : Type u_1} {ι : Type u_3} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype PauliType] [DecidableEq PauliType] {A : Type u_4} {B : Type u_5} [Fintype A] [Fintype B] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) ι 3) (D : CL.Detyping.Question (QuestionType PauliType ℓ) ι → CL.Detyping.Question (QuestionType PauliType ℓ) ι → A → B → Bool) :
      (game E X Z ℓ P D).μ (QuestionType.introspect false, 0) (QuestionType.introspect true, 0) = (↑(TypeGraph.edges E X Z ℓ).card)⁻¹

      The cross-introspection test occurs at exactly the inverse ordered-edge count.

      source
      theorem MIPRE.Introspection.TypedPresentation.failAt_aux_le {PauliType : Type u_1} {ι : Type u_3} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype PauliType] [DecidableEq PauliType] {A : Type u_4} {B : Type u_5} [Fintype A] [Fintype B] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) ι 3) (D : CL.Detyping.Question (QuestionType PauliType ℓ) ι → CL.Detyping.Question (QuestionType PauliType ℓ) ι → A → B → Bool) (S : TensorProductStrategy (game E X Z ℓ P D)) (t u : AuxType ℓ) (w w' : Bool) (h : TypeGraph.Adj E X Z (Sum.inr (t, w)) (Sum.inr (u, w'))) :
      S.failAt (Sum.inr (t, w), 0) (Sum.inr (u, w'), 0) ≤ ↑(TypeGraph.edges E X Z ℓ).card * (1 - S.value)

      Failure on one auxiliary edge is bounded by the ordered-edge count times total failure.

      source
      theorem MIPRE.Introspection.TypedPresentation.failAt_cross_introspect_le {PauliType : Type u_1} {ι : Type u_3} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype PauliType] [DecidableEq PauliType] {A : Type u_4} {B : Type u_5} [Fintype A] [Fintype B] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) ι 3) (D : CL.Detyping.Question (QuestionType PauliType ℓ) ι → CL.Detyping.Question (QuestionType PauliType ℓ) ι → A → B → Bool) (S : TensorProductStrategy (game E X Z ℓ P D)) {ε : ℝ} (hS : 1 - ε ≤ S.value) :
      S.failAt (QuestionType.introspect false, 0) (QuestionType.introspect true, 0) ≤ ↑(TypeGraph.edges E X Z ℓ).card * ε

      Near-perfect typed play gives the cross-introspection bound used in extraction.