The executable representative is the Pauli sampler's canonical point

This bridge identifies the uniform Shoup program with the actual canonLin used by both axis and diagonal question maps, including the zero direction.

theorem MIPRE.QLD.PauliCL.representative_eq_canonLin {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (u v : Fin n → F) : Introspection.LineProgram.representative u v = (CL.canonLin (F ∙ v)) u

theorem MIPRE.QLD.PauliCL.lineRepresentativeProg_canonLin (k : ℕ) (hk : 1 ≤ k) {n : ℕ} (u v : Fin n → (SAT.shoupBinField k hk).carrier) : Introspection.LineProgram.lineRepresentativeProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).vecBits u, (SAT.shoupBinField k hk).vecBits v) = (SAT.shoupBinField k hk).vecBits ((CL.canonLin ((SAT.shoupBinField k hk).carrier ∙ v)) u)

The actual total polynomial-time program computes the canonical base point used in the seeded axis and diagonal Pauli questions.