Documentation

MIPRE.Background.QLD.PauliAnswerCoding

Canonical Pauli answer payloads and their semantic decoding #

Each type fixes its answer constructor. Field vectors use canonical field blocks, polynomials use ascending coefficients, and full Pauli answers use the same little-endian cube enumeration as the executable table evaluator.

source
noncomputable def MIPRE.QLD.PauliAnswerProgram.answerRows {k m d : ℕ} (E : SAT.BinField k) :
Answer E.carrier m d → List Cost.BitStr
Equations
Instances For
    source
    noncomputable def MIPRE.QLD.PauliAnswerProgram.answerBits {k m d : ℕ} (E : SAT.BinField k) (a : Answer E.carrier m d) :
    Cost.BitStr
    Equations
    Instances For
      source
      noncomputable def MIPRE.QLD.PauliAnswerProgram.decodeRows {k : ℕ} (E : SAT.BinField k) (m d : ℕ) (T : Ty) (rows : List Cost.BitStr) :
      Answer E.carrier m d
      Equations
      Instances For
        source
        theorem MIPRE.QLD.PauliAnswerProgram.decodeRows_format {k m d : ℕ} (E : SAT.BinField k) (q : Question E.carrier m) (rows : List Cost.BitStr) :
        q.fmtOk (decodeRows E m d q.ty rows) = true
        source
        theorem MIPRE.QLD.PauliAnswerProgram.answerRows_length {k m d : ℕ} (E : SAT.BinField k) (q : Question E.carrier m) (a : Answer E.carrier m d) (h : q.fmtOk a = true) :
        (answerRows E a).length = count q.ty m d
        source
        theorem MIPRE.QLD.PauliAnswerProgram.answerRows_width {k m d : ℕ} (E : SAT.BinField k) (q : Question E.carrier m) (a : Answer E.carrier m d) (h : q.fmtOk a = true) (row : Cost.BitStr) :
        row ∈ answerRows E a → List.length row = width q.ty k
        source
        theorem MIPRE.QLD.PauliAnswerProgram.fieldRow {k n : ℕ} (E : SAT.BinField k) (v : Fin n → E.carrier) (i : Fin n) :
        (E.vecBits v).getD ↑i [] = E.toBits (v i)
        source
        theorem MIPRE.QLD.PauliAnswerProgram.decodeRows_answerRows {k m d : ℕ} (E : SAT.BinField k) (q : Question E.carrier m) (a : Answer E.carrier m d) (h : q.fmtOk a = true) :
        decodeRows E m d q.ty (answerRows E a) = a
        source
        theorem MIPRE.QLD.PauliAnswerProgram.parser_answerBits {k m d : ℕ} (E : SAT.BinField k) (hk : 0 < k) (q : Question E.carrier m) (a : Answer E.carrier m d) (h : q.fmtOk a = true) :
        parser.toFun (q.ty, Cost.unary m, Cost.unary k, Cost.unary d, answerBits E a) = (true, answerRows E a)
        source
        noncomputable def MIPRE.QLD.PauliAnswerProgram.decodeBits {k : ℕ} (E : SAT.BinField k) (m d : ℕ) (T : Ty) (bs : Cost.BitStr) :
        Answer E.carrier m d
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem MIPRE.QLD.PauliAnswerProgram.decodeBits_answerBits {k m d : ℕ} (E : SAT.BinField k) (hk : 0 < k) (q : Question E.carrier m) (a : Answer E.carrier m d) (h : q.fmtOk a = true) :
          decodeBits E m d q.ty (answerBits E a) = a
          source
          theorem MIPRE.QLD.PauliAnswerProgram.answerBits_injective_of_format {k m d : ℕ} (E : SAT.BinField k) (hk : 0 < k) (q : Question E.carrier m) (a b : Answer E.carrier m d) (ha : q.fmtOk a = true) (hb : q.fmtOk b = true) :
          answerBits E a = answerBits E b ↔ a = b

          Payload equality is faithful within every prescribed answer format.