Exact decision equality for every pair of Pauli types

The arithmetic branches are proved individually. The fixed finite type router then selects a forward branch, its proved reversal, exact consistency, or the legacy off-graph default. Question contents remain arbitrary throughout.

theorem MIPRE.QLD.PauliBooleanProgram.pairTest_unhandled {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] (hm : m ∣ Fintype.card F) (x y : Question F m) (a b : Answer F m d) (h : handled x.ty y.ty = false) : pairTest hm x y a b = true

theorem MIPRE.QLD.PauliBooleanProgram.program_correct_forward (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (hj : j ≤ k) (hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier) (T U : Ty) (x y : PauliCL.Coord (2 ^ j) → (SAT.shoupBinField k hk).carrier) (a b : Answer (SAT.shoupBinField k hk).carrier (2 ^ j) 1) (ha : (PauliCL.ExplicitSeed.decode (PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) T x).fmtOk a = true) (hb : (PauliCL.ExplicitSeed.decode (PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) U y).fmtOk b = true) (hf : Forward T U) (reverse : Bool) : program.toFun (encodedInput (SAT.shoupBinField k hk) j T U x y a b) = if reverse = true then accepts hm (PauliCL.ExplicitSeed.decode (PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) U y) (PauliCL.ExplicitSeed.decode (PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) T x) b a else accepts hm (PauliCL.ExplicitSeed.decode (PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) T x) (PauliCL.ExplicitSeed.decode (PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) U y) a b

theorem MIPRE.QLD.PauliBooleanProgram.program_correct_formatted (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (hj : j ≤ k) (hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier) (T U : Ty) (x y : PauliCL.Coord (2 ^ j) → (SAT.shoupBinField k hk).carrier) (a b : Answer (SAT.shoupBinField k hk).carrier (2 ^ j) 1) (ha : (PauliCL.ExplicitSeed.decode (PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) T x).fmtOk a = true) (hb : (PauliCL.ExplicitSeed.decode (PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) U y).fmtOk b = true) : program.toFun (encodedInput (SAT.shoupBinField k hk) j T U x y a b) = accepts hm (PauliCL.ExplicitSeed.decode (PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) T x) (PauliCL.ExplicitSeed.decode (PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) U y) a b

The executable Pauli predicate agrees with the transported QLD interface on all raw question contents and all canonically encoded formatted answers.