Full-register projection of every valid raw Pauli answer

noncomputable def MIPRE.QLD.PauliFullAnswerProgram.decodedOutcome {k : ℕ} (E : SAT.BinField k) (m : ℕ) (W : Bas) (bs : Cost.BitStr) : (Fin m → Bool) → E.carrier

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.QLD.PauliFullAnswerProgram.decodeBits_pauli {k : ℕ} (E : SAT.BinField k) (m : ℕ) (W : Bas) (bs : Cost.BitStr) : PauliAnswerProgram.decodeBits E m 1 (Ty.pauli W) bs = Answer.pauliAns (decodedOutcome E m W bs)

theorem MIPRE.QLD.PauliFullAnswerProgram.program_raw (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (m : ℕ) (W : Bas) (bs : Cost.BitStr) (hvalid : (PauliAnswerProgram.parser.toFun (Ty.pauli W, Cost.unary m, Cost.unary k, Cost.unary 1, bs)).1 = true) : program.toFun (Cost.unary m, Cost.unary k, bs) = (true, CL.toBits (registerVector (SAT.shoupSelfDualNormalBasis k hk hodd) (decodedOutcome (SAT.shoupBinField k hk) m W bs)))