Documentation

MIPRE.Background.QLD.CLExplicitTransport

Equivalences between explicit and legacy Pauli question contents #

Only line questions carry the seed. Permuting that coordinate on their raw contents gives a genuine equivalence, including contents outside the support of the sampler. The same permutation of the shared random seed intertwines all twenty-six sampled question maps simultaneously.

source
def MIPRE.QLD.PauliCL.ExplicitSeed.vectorPermutation {F : Type u_1} {m : ℕ} (π : F ≃ F) :
(Coord m → F) ≃ (Coord m → F)

Change the field seed coordinate and leave every other coordinate intact.

Equations
Instances For
    source
    theorem MIPRE.QLD.PauliCL.ExplicitSeed.vectorPermutation_content {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (π : F ≃ F) (c : Content F m) :
    (vectorPermutation π) (contentVector c) = contentVector ((contentPermutation π) c)
    source
    def MIPRE.QLD.PauliCL.ExplicitSeed.outputPermutation {F : Type u_1} {m : ℕ} (π : F ≃ F) :
    Ty → (Coord m → F) ≃ (Coord m → F)

    Raw output-question equivalence; only the two line families retain a seed.

    Equations
    Instances For
      source
      theorem MIPRE.QLD.PauliCL.ExplicitSeed.questionOfVector_outputPermutation {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (π : F ≃ F) (T : Ty) (x : Coord m → F) :
      questionOfVector T ((outputPermutation π T) x) = decode π T x
      source
      theorem MIPRE.QLD.PauliCL.ExplicitSeed.outputPermutation_presentation {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (χ : F → Fin m) (π : F ≃ F) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) (T : Ty) (c : Content F m) :
      (outputPermutation π T) ((presentation χ T).eval (contentVector c)) = (PauliCL.presentation hm T).eval (contentVector ((contentPermutation π) c))
      source
      noncomputable def MIPRE.QLD.PauliCL.ExplicitSeed.binaryOutputPermutation {F : Type u_1} [Field F] {m : ℕ} [Algebra (ZMod 2) F] {t : ℕ} (π : F ≃ F) (b : Module.Basis (Fin t) (ZMod 2) F) (T : Ty) :
      (Fin ((3 * m + 3) * t) → ZMod 2) ≃ (Fin ((3 * m + 3) * t) → ZMod 2)

      Raw binary output-question equivalence, in the supplied basis.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MIPRE.QLD.PauliCL.ExplicitSeed.binarySeedPermutation {F : Type u_1} [Field F] {m : ℕ} [Algebra (ZMod 2) F] {t : ℕ} (π : F ≃ F) (b : Module.Basis (Fin t) (ZMod 2) F) :
        (Fin ((3 * m + 3) * t) → ZMod 2) ≃ (Fin ((3 * m + 3) * t) → ZMod 2)

        The corresponding permutation of the common binary random content.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem MIPRE.QLD.PauliCL.ExplicitSeed.binaryQuestion_outputPermutation {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] [Algebra (ZMod 2) F] {t : ℕ} (π : F ≃ F) (b : Module.Basis (Fin t) (ZMod 2) F) (T : Ty) (x : Fin ((3 * m + 3) * t) → ZMod 2) :
          binaryQuestion b T ((binaryOutputPermutation π b T) x) = binaryDecode π b T x
          source
          theorem MIPRE.QLD.PauliCL.ExplicitSeed.binaryOutputPermutation_presentation {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] [Algebra (ZMod 2) F] {t : ℕ} (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) (T : Ty) (x : Fin ((3 * m + 3) * t) → ZMod 2) :
          (binaryOutputPermutation π b T) ((binaryPresentation χ b T).eval x) = (PauliCL.binaryPresentation hm b T).eval ((binarySeedPermutation π b) x)
          source
          @[simp]
          theorem MIPRE.QLD.PauliCL.ExplicitSeed.binaryOutputPermutation_pauli {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] [Algebra (ZMod 2) F] {t : ℕ} (π : F ≃ F) (b : Module.Basis (Fin t) (ZMod 2) F) (W : Bas) (x : Fin ((3 * m + 3) * t) → ZMod 2) :
          (binaryOutputPermutation π b (Ty.pauli W)) x = x