Pauli semantics of the actual prepared decision kernel

theorem MIPRE.Introspection.DecisionKernel.canonical_canonicalInput (V : Verifier 7) (lam n Q R : ℕ) (p : PauliSamplerParameters.Parameters) (T U : Label) (x y a b : Cost.BitStr) : canonical.toFun (canonicalInput V lam n Q R p T U x y a b) = true

theorem MIPRE.Introspection.DecisionKernel.questionLengths_canonicalInput (V : Verifier 7) (lam n Q R : ℕ) (p : PauliSamplerParameters.Parameters) (T U : Label) (x y a b : Cost.BitStr) : questionLengths.toFun (canonicalInput V lam n Q R p T U x y a b) = true ↔ List.length x = (3 * List.length p.2.2 + 3) * List.length p.1 ∧ List.length y = (3 * List.length p.2.2 + 3) * List.length p.1

theorem MIPRE.Introspection.DecisionKernel.leftPauliFormat_canonicalInput (V : Verifier 7) (lam n Q R : ℕ) (p : PauliSamplerParameters.Parameters) (U : Label) (x y a b : Cost.BitStr) (t : QLD.Ty) : leftPauliFormat.toFun (canonicalInput V lam n Q R p (Sum.inl t) U x y a b) = QLD.PauliBinaryProgram.endpointValid.toFun (p, t, x, a)

theorem MIPRE.Introspection.DecisionKernel.rightPauliFormat_canonicalInput (V : Verifier 7) (lam n Q R : ℕ) (p : PauliSamplerParameters.Parameters) (T : Label) (x y a b : Cost.BitStr) (u : QLD.Ty) : rightPauliFormat.toFun (canonicalInput V lam n Q R p T (Sum.inl u) x y a b) = QLD.PauliBinaryProgram.endpointValid.toFun (p, u, y, b)

theorem MIPRE.Introspection.DecisionKernel.pauli_canonicalInput (V : Verifier 7) (lam n Q R : ℕ) (p : PauliSamplerParameters.Parameters) (x y a b : Cost.BitStr) (t u : QLD.Ty) : pauli.toFun (canonicalInput V lam n Q R p (Sum.inl t) (Sum.inl u) x y a b) = QLD.PauliBinaryProgram.program.toFun (p, (t, x, a), u, y, b)

theorem MIPRE.Introspection.DecisionKernel.program_pauli_iff (V : Verifier 7) (lam n Q R : ℕ) (x y a b : Cost.BitStr) (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) (hx : List.length x = (3 * 2 ^ j + 3) * k) (hy : List.length y = (3 * 2 ^ j + 3) * k) : have p := (Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)); (program W).toFun (canonicalInput V lam n Q R p (Sum.inl t) (Sum.inl u) x y a b) = true ↔ QLD.PauliBinaryProgram.endpointValid.toFun (p, t, x, a) = true ∧ QLD.PauliBinaryProgram.endpointValid.toFun (p, u, y, b) = true ∧ QLD.accepts hm (QLD.PauliBinaryProgram.questionOfBits k hk hodd j t x) (QLD.PauliBinaryProgram.questionOfBits k hk hodd j u y) (QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) (2 ^ j) 1 t a) (QLD.PauliAnswerProgram.decodeBits (SAT.shoupBinField k hk) (2 ^ j) 1 u b) = true ∧ (auxiliary W).toFun (canonicalInput V lam n Q R p (Sum.inl t) (Sum.inl u) x y a b) = true

Every actual Pauli-pair computation agrees with QLD on the decoded raw bytes.

theorem MIPRE.Introspection.DecisionKernel.project_canonicalInput (V : Verifier 7) (lam n Q R : ℕ) (a b : Cost.BitStr) (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j m : ℕ) (W : QLD.Bas) (u : Label) (ha : (QLD.PauliAnswerProgram.parser.toFun (QLD.Ty.pauli W, Cost.unary m, Cost.unary k, Cost.unary 1, a)).1 = true) : project.toFun (AuxiliaryDecision.canonical V lam n Q R (Cost.unary k, Cost.unary j, Cost.unary m) (Sum.inl (QLD.Ty.pauli W)) u a b) = CL.toBits (QLD.PauliFullAnswerProgram.registerVector (SAT.shoupSelfDualNormalBasis k hk hodd) (QLD.PauliFullAnswerProgram.decodedOutcome (SAT.shoupBinField k hk) m W a))

The callback uses the same explicit full-register numbering as the semantic Pauli outcome.