The introspection kernel's Pauli conjunct as controlled linear constraints

MIPRE.Introspection.DecisionKernel.program_pauli_iff reads the decision kernel, at a pair of Pauli labels, as two endpoint-validity checks, the Pauli basis test on the decoded questions and answers, and the auxiliary conjunct. program_pauli_iff_cons replaces the first three by the answer lengths of the tailored layout (pauliLen) and the satisfaction of the controlled linear constraints pauliCons (MIPRE/Background/Tailored/Intro/PauliCons.lean), which is the form the tailored presentation of the introspection verifier consumes.

theorem MIPRE.Tailored.Intro.PauliCons.program_pauli_iff_cons (V : Verifier 7) (lam n Q R : ℕ) (W : Cost.ClockedUniversalMachine) (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (hj : j ≤ k) (hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier) (t u : QLD.Ty) (x y a b : Cost.BitStr) (hx : List.length x = (3 * 2 ^ j + 3) * k) (hy : List.length y = (3 * 2 ^ j + 3) * k) : (Introspection.DecisionKernel.program W).toFun (Introspection.DecisionKernel.canonicalInput V lam n Q R (Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)) (Sum.inl t) (Sum.inl u) x y a b) = true ↔ List.length a = pauliLen (2 ^ j) k t ∧ List.length b = pauliLen (2 ^ j) k u ∧ (∀ c ∈ pauliCons k hk hodd j hm t u x y (List.take (pauliLenR k (2 ^ j) t) a) (List.take (pauliLenR k (2 ^ j) u) b), Satisfies c (a ++ b ++ [true])) ∧ (Introspection.DecisionKernel.auxiliary W).toFun (Introspection.DecisionKernel.canonicalInput V lam n Q R (Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)) (Sum.inl t) (Sum.inl u) x y a b) = true

The kernel at a pair of Pauli labels is the tailored check. The decision kernel accepts exactly when both answers have their label's length, the constraints of pauliCons at the readable prefixes are satisfied, and the auxiliary conjunct holds.