The Pauli labels of the tailored question reduction

The Pauli basis test's answers keep their byte encodings in the tailored layout (MIPRE.Tailored.Intro.enc): a label T has count T m 1 blocks of width T k bits (QLD.PauliAnswerProgram), all readable at the Z-basis Pauli label and all linear otherwise.

def MIPRE.Tailored.Intro.pauliLen (m k : ℕ) (T : QLD.Ty) : ℕ

The number of answer bits of a Pauli label, for registers of 2^m field elements of k bits, at degree 1.

Equations

• MIPRE.Tailored.Intro.pauliLen m k T = MIPRE.QLD.PauliAnswerProgram.count T m 1 * MIPRE.QLD.PauliAnswerProgram.width T k

def MIPRE.Tailored.Intro.pauliRead : QLD.Ty → Bool

The readable Pauli label: the Z-basis Pauli answer.

Equations

• MIPRE.Tailored.Intro.pauliRead (MIPRE.QLD.Ty.pauli MIPRE.QLD.Bas.Z) = true
• MIPRE.Tailored.Intro.pauliRead x✝ = false

theorem MIPRE.Tailored.Intro.pauliLen_pauli (m k : ℕ) (W : QLD.Bas) : pauliLen m k (QLD.Ty.pauli W) = 2 ^ m * k