Faithful extraction of the Pauli question's arithmetic fields

The basis metadata from finite routing selects the corresponding point and scalar. The explicit axis direction agrees with the original game after the same seed permutation used by the sampled-game transport.

theorem MIPRE.QLD.PauliQuestionProgram.selectedPoint_fieldEncoding {k m : ℕ} (E : SAT.BinField k) (W : Bas) (x : PauliCL.Coord m → E.carrier) : Introspection.FieldQuestionProgram.selectedPoint.toFun (PauliBranchProgram.basisIndex W, PauliCL.fieldEncoding E x) = E.vecBits fun (i : Fin m) => x (PauliCL.Coord.point W i)

theorem MIPRE.QLD.PauliQuestionProgram.selectedScalar_fieldEncoding {k m : ℕ} (E : SAT.BinField k) (W : Bas) (x : PauliCL.Coord m → E.carrier) : Introspection.FieldQuestionProgram.selectedScalar.toFun (PauliBranchProgram.basisIndex W, PauliCL.fieldEncoding E x) = E.toBits (x (PauliCL.Coord.scalar W))

theorem MIPRE.QLD.PauliQuestionProgram.axisDirectionProg_legacy (k : ℕ) (hk : 1 ≤ k) (j : ℕ) (hj : j ≤ k) (hm : 2 ^ j ∣ Fintype.card (SAT.shoupBinField k hk).carrier) (s : (SAT.shoupBinField k hk).carrier) : Introspection.FieldQuestionProgram.axisDirectionProg.toFun ((Cost.unary k, Cost.unary j, Cost.unary (2 ^ j)), (SAT.shoupBinField k hk).toBits s) = (SAT.shoupBinField k hk).vecBits (Pi.single (LIDT.CL.chi hm ((PauliCL.ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) s)) 1)

The line program uses precisely the legacy game's selected axis under its proved seed change, rather than assuming a finite enumeration is computable.

theorem MIPRE.QLD.PauliQuestionProgram.gammaProg_fieldEncoding (k : ℕ) (hk : 1 ≤ k) {m : ℕ} (x : PauliCL.Coord m → (SAT.shoupBinField k hk).carrier) : Introspection.FieldGammaProgram.gammaProg.toFun (Cost.unary k, (Introspection.PauliStageProgram.pointX.toFun (PauliCL.fieldEncoding (SAT.shoupBinField k hk) x)).zip (Introspection.PauliStageProgram.pointZ.toFun (PauliCL.fieldEncoding (SAT.shoupBinField k hk) x)), Introspection.PauliStageProgram.scalarX.toFun (PauliCL.fieldEncoding (SAT.shoupBinField k hk) x), Introspection.PauliStageProgram.scalarZ.toFun (PauliCL.fieldEncoding (SAT.shoupBinField k hk) x)) = LowDegree.BinaryLinear.bit (gam (PauliCL.vectorContent x).omega)