Identification of the kernel's finite semantics with the explicit game

theorem MIPRE.Introspection.DecisionKernel.finitePauliCheck_toBits (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier) (x y : Fin ((3 * 2 ^ j + 3) * k) → CL.𝔽₂) (T U : QLD.Ty) : finitePauliCheck k hk hodd j hm (CL.toBits x) (CL.toBits y) T U = ExplicitGame.pauliCheck hm (QLD.PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) (SAT.shoupSelfDualNormalBasis k hk hodd) T U x y

theorem MIPRE.Introspection.DecisionKernel.pauliProject_eq_numbered {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m k : ℕ} (basis : Module.Basis (Fin k) (ZMod 2) F) (a : QLD.Answer F m 1) : Answer.pauliProject basis a = fun (i : Fin (2 ^ m * k)) => BinaryComplete.project basis a ((QLD.PauliFullAnswerProgram.registerNumbering m k).symm i)

theorem MIPRE.Introspection.DecisionKernel.program_sound_numbered (W : Cost.ClockedUniversalMachine) {lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (j : ℕ) (hj : j ≤ k) (hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier) (hs : V.sampler.dim (2 ^ n) ≤ 2 ^ 2 ^ j * k) (hQ : 4 ≤ 2 ^ 2 ^ j * k) (hR : 3 * (2 ^ n) ^ lam ≤ 2 ^ 2 ^ j * k) (χ : (SAT.shoupBinField k hk).carrier → Fin (2 ^ j)) (T U : Label) (x y : Fin ((3 * 2 ^ j + 3) * k) → CL.𝔽₂) (a b : Cost.BitStr) (h : (program W).toFun (canonicalInput V lam n (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) (Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)) T U (CL.toBits x) (CL.toBits y) a b) = true) : (NumberedComplete.game (QLD.PauliFullAnswerProgram.registerNumbering (2 ^ j) k).symm (AuxiliaryDecision.padded V hs) (finiteSourcePredicate V hs) hm (SAT.shoupSelfDualNormalBasis k hk hodd) χ (QLD.PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk))).D (T, x) (U, y) (Answer.decode (SAT.shoupBinField k hk) (2 ^ j) (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) T a) (Answer.decode (SAT.shoupBinField k hk) (2 ^ j) (2 ^ 2 ^ j * k) ((2 ^ n) ^ lam) U b) = true

Raw kernel acceptance gives the exact finite game used by the source soundness theorem, including the executable full-register numbering.