Documentation

MIPRE.Background.QLD.CLPresentation

The actual three-level Pauli question presentations #

The ambient coordinates are precisely the two points, the seed, the raw direction, and the two scalars in Content. The presentation reads the seed, then the selected direction, then the point and scalar registers. Its full evaluation is the question map of the existing twenty-six-type Pauli game. These are concrete field-valued presentations; uniform binary execution is a separate layer.

source
inductive MIPRE.QLD.PauliCL.Coord (m : ℕ) :
Type

The 3m+3 field coordinates in the actual Pauli sample.

Instances For
    source
    @[instance_reducible]
    instance MIPRE.QLD.PauliCL.instDecidableEqCoord {m✝ : ℕ} :
    DecidableEq (Coord m✝)
    Equations
    source
    def MIPRE.QLD.PauliCL.instDecidableEqCoord.decEq {m✝ : ℕ} (x✝ x✝¹ : Coord m✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance MIPRE.QLD.PauliCL.instFintypeCoord {m✝ : ℕ} :
      Fintype (Coord m✝)
      Equations
      source
      def MIPRE.QLD.PauliCL.coordEquiv (m : ℕ) :
      Coord m ≃ Bas × Fin m ⊕ Unit ⊕ Fin m ⊕ Bas
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def MIPRE.QLD.PauliCL.contentVector {F : Type u_1} {m : ℕ} (c : Content F m) :
        Coord m → F
        Equations
        Instances For
          source
          def MIPRE.QLD.PauliCL.vectorContent {F : Type u_1} {m : ℕ} (x : Coord m → F) :
          Content F m
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def MIPRE.QLD.PauliCL.contentEquiv {F : Type u_1} {m : ℕ} :
            Content F m ≃ (Coord m → F)
            Equations
            Instances For
              source
              def MIPRE.QLD.PauliCL.seedSet (m : ℕ) :
              Finset (Coord m)
              Equations
              Instances For
                source
                noncomputable def MIPRE.QLD.PauliCL.directionSet (m : ℕ) :
                Finset (Coord m)
                Equations
                Instances For
                  source
                  noncomputable def MIPRE.QLD.PauliCL.finalSet (m : ℕ) :
                  Finset (Coord m)
                  Equations
                  Instances For
                    source
                    theorem MIPRE.QLD.PauliCL.direction_subset (m : ℕ) :
                    directionSet m ⊆ Finset.univ \ seedSet m
                    source
                    theorem MIPRE.QLD.PauliCL.remainder_eq (m : ℕ) :
                    (Finset.univ \ seedSet m) \ directionSet m = finalSet m
                    source
                    def MIPRE.QLD.PauliCL.pointMap {F : Type u_1} [Field F] {m : ℕ} (W : Bas) (L : (Fin m → F) →ₗ[F] Fin m → F) :
                    CL.RegLinear F (finalSet m)

                    A point-register linear map, zero on all other content coordinates.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def MIPRE.QLD.PauliCL.directionMap {F : Type u_1} [Field F] {m : ℕ} (i : Fin m) :
                      CL.RegLinear F (directionSet m)
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def MIPRE.QLD.PauliCL.seedMap {F : Type u_1} [Field F] {m : ℕ} :
                        Ty → CL.RegLinear F (seedSet m)
                        Equations
                        Instances For
                          source
                          @[simp]
                          theorem MIPRE.QLD.PauliCL.pointMap_apply {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (W : Bas) (L : (Fin m → F) →ₗ[F] Fin m → F) (x : Coord m → F) (c : Coord m) :
                          (pointMap W L) x c = match c with | Coord.point W' i => if W' = W then L (fun (j : Fin m) => x (Coord.point W j)) i else 0 | x => 0
                          source
                          @[simp]
                          theorem MIPRE.QLD.PauliCL.directionMap_apply {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (i : Fin m) (x : Coord m → F) (c : Coord m) :
                          (directionMap i) x c = match c with | Coord.direction j => if j < i then 0 else x (Coord.direction j) | x => 0
                          source
                          noncomputable def MIPRE.QLD.PauliCL.secondMap {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (t : Ty) (s : F) :
                          CL.RegLinear F (directionSet m)
                          Equations
                          Instances For
                            source
                            noncomputable def MIPRE.QLD.PauliCL.finalMap {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (t : Ty) (s : F) (v : Fin m → F) :
                            CL.RegLinear F (finalSet m)
                            Equations
                            Instances For
                              source
                              noncomputable def MIPRE.QLD.PauliCL.presentation {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (t : Ty) :
                              CL.CLFun F (Coord m) 3

                              All twenty-six full question maps, with an explicit three-stage register partition. Trivial stages are retained for the lower-level question types.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                theorem MIPRE.QLD.PauliCL.presentation_exactlyOn {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (t : Ty) :
                                (presentation hm t).ExactlyOn Finset.univ
                                source
                                def MIPRE.QLD.PauliCL.questionOfVector {F : Type u_1} {m : ℕ} (t : Ty) (x : Coord m → F) :
                                Question F m

                                Decode the actual content carried by a question of the specified type.

                                Equations
                                Instances For
                                  source
                                  theorem MIPRE.QLD.PauliCL.questionOfVector_presentation {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (t : Ty) (c : Content F m) :
                                  questionOfVector t ((presentation hm t).eval (contentVector c)) = Content.question hm c t

                                  Full evaluation produces exactly the seeded question in QLD.Game, including its seed-dependent diagonal direction and canonical base point.

                                  source
                                  theorem MIPRE.QLD.PauliCL.presentation_pauli_eval {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (W : Bas) (x : Coord m → F) :
                                  (presentation hm (Ty.pauli W)).eval x = 0

                                  Full Pauli questions have the literal zero content needed by the introspection sampling and first-hiding edges.

                                  source
                                  def MIPRE.QLD.PauliCL.sampleEquiv {F : Type u_1} {m : ℕ} :
                                  Sample F m ≃ TyEdge × (Coord m → F)

                                  Numbering the existing random content preserves its uniform law.

                                  Equations
                                  Instances For
                                    source
                                    theorem MIPRE.QLD.PauliCL.qldGame_mu_presentation {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} [NeZero m] [Algebra (ZMod 2) F] {d : ℕ} (hm : m ∣ Fintype.card F) (x y : Question F m) :
                                    (qldGame hm).μ x y = SampledGame.dist (fun (p : TyEdge × (Coord m → F)) => questionOfVector (↑p.1).1 ((presentation hm (↑p.1).1).eval p.2)) (fun (p : TyEdge × (Coord m → F)) => questionOfVector (↑p.1).2 ((presentation hm (↑p.1).2).eval p.2)) x y

                                    The actual Pauli game's question law is generated by the constructed CL family, using a uniformly chosen graph edge and a common ambient vector.