Documentation

MIPRE.Background.QLD.PauliAnswerPrograms

Faithful type-directed Pauli answer parsing #

The exact question type is retained. Only the answer shape is shared by types with identical formats. Counts are checked before any field table is allocated; in particular the full Pauli count stays binary. The degree is supplied in unary (and is the fixed constant one in the introspection application).

source
def MIPRE.QLD.PauliAnswerProgram.shape :
Ty → ℕ
Equations
Instances For
    source
    def MIPRE.QLD.PauliAnswerProgram.count (T : Ty) (m d : ℕ) :
    ℕ
    Equations
    Instances For
      source
      def MIPRE.QLD.PauliAnswerProgram.width (T : Ty) (k : ℕ) :
      ℕ
      Equations
      Instances For
        source
        noncomputable def MIPRE.QLD.PauliAnswerProgram.flattenUnary :
        Cost.PolyTimeFun (List Cost.Unary) Cost.Unary
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def MIPRE.QLD.PauliAnswerProgram.productUnary :
          Cost.PolyTimeFun (Cost.Unary × Cost.Unary) Cost.Unary
          Equations
          Instances For
            source
            theorem MIPRE.QLD.PauliAnswerProgram.productUnary_length (m d : Cost.Unary) :
            List.length (productUnary.toFun (m, d)) = List.length m * List.length d
            source
            @[reducible, inline]
            abbrev MIPRE.QLD.PauliAnswerProgram.Input :
            Type
            Equations
            Instances For
              source
              noncomputable def MIPRE.QLD.PauliAnswerProgram.kind :
              Cost.PolyTimeFun Input ℕ
              Equations
              Instances For
                source
                noncomputable def MIPRE.QLD.PauliAnswerProgram.dimension :
                Cost.PolyTimeFun Input Cost.Unary
                Equations
                Instances For
                  source
                  noncomputable def MIPRE.QLD.PauliAnswerProgram.fieldWidth :
                  Cost.PolyTimeFun Input Cost.Unary
                  Equations
                  Instances For
                    source
                    noncomputable def MIPRE.QLD.PauliAnswerProgram.degree :
                    Cost.PolyTimeFun Input Cost.Unary
                    Equations
                    Instances For
                      source
                      noncomputable def MIPRE.QLD.PauliAnswerProgram.answer :
                      Cost.PolyTimeFun Input Cost.BitStr
                      Equations
                      Instances For
                        source
                        noncomputable def MIPRE.QLD.PauliAnswerProgram.isKind (i : ℕ) :
                        Cost.PolyTimeFun Input Bool
                        Equations
                        Instances For
                          source
                          noncomputable def MIPRE.QLD.PauliAnswerProgram.countProg :
                          Cost.PolyTimeFun Input ℕ
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            noncomputable def MIPRE.QLD.PauliAnswerProgram.widthProg :
                            Cost.PolyTimeFun Input Cost.Unary
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              theorem MIPRE.QLD.PauliAnswerProgram.countProg_apply (T : Ty) (m k d : Cost.Unary) (bs : Cost.BitStr) :
                              countProg.toFun (T, m, k, d, bs) = count T (List.length m) (List.length d)
                              source
                              theorem MIPRE.QLD.PauliAnswerProgram.widthProg_length (T : Ty) (m k d : Cost.Unary) (bs : Cost.BitStr) :
                              List.length (widthProg.toFun (T, m, k, d, bs)) = width T (List.length k)
                              source
                              noncomputable def MIPRE.QLD.PauliAnswerProgram.parser :
                              Cost.PolyTimeFun Input (Bool × List Cost.BitStr)
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                theorem MIPRE.QLD.PauliAnswerProgram.parser_flatten (T : Ty) (m k d : Cost.Unary) (rows : List Cost.BitStr) (hk : 0 < width T (List.length k)) (hn : rows.length = count T (List.length m) (List.length d)) (hw : ∀ row ∈ rows, List.length row = width T (List.length k)) :
                                parser.toFun (T, m, k, d, rows.flatten) = (true, rows)

                                Every canonical payload is returned exactly, including the unit-width bit rows.