Correctness of the executable seeded Pauli line stages #
The fixed axis and diagonal programs compute the precise canonical maps in the explicit-selector CL presentation. The legacy forms also identify their output with the original QLD line maps after the proved seed permutation.
theorem
MIPRE.QLD.PauliCL.axisRepresentativeProg_canonLin
(k : ℕ)
(hk : 1 ≤ k)
(j : ℕ)
(hj : j ≤ k)
(s : (SAT.shoupBinField k hk).carrier)
(u : Fin (2 ^ j) → (SAT.shoupBinField k hk).carrier)
:
Introspection.SeededLineProgram.axisRepresentativeProg.toFun
((Cost.unary k, Cost.unary j, (SAT.shoupBinField k hk).toBits s), (SAT.shoupBinField k hk).vecBits u) = (SAT.shoupBinField k hk).vecBits
((CL.canonLin
((SAT.shoupBinField k hk).carrier ∙ Pi.single (Introspection.SeedProgram.selector (SAT.shoupBinField k hk) j hj s) 1))
u)
theorem
MIPRE.QLD.PauliCL.diagonalRepresentativeProg_canonLin
(k : ℕ)
(hk : 1 ≤ k)
(j : ℕ)
(hj : j ≤ k)
(s : (SAT.shoupBinField k hk).carrier)
(u v : Fin (2 ^ j) → (SAT.shoupBinField k hk).carrier)
:
have v' := fun (i : Fin (2 ^ j)) =>
if i < Introspection.SeedProgram.selector (SAT.shoupBinField k hk) j hj s then 0 else v i;
Introspection.SeededLineProgram.diagonalRepresentativeProg.toFun
((Cost.unary k, Cost.unary j, (SAT.shoupBinField k hk).toBits s), (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), (SAT.shoupBinField k hk).vecBits v')
theorem
MIPRE.QLD.PauliCL.axisRepresentativeProg_legacy
(k : ℕ)
(hk : 1 ≤ k)
(j : ℕ)
(hj : j ≤ k)
(s : (SAT.shoupBinField k hk).carrier)
(u : Fin (2 ^ j) → (SAT.shoupBinField k hk).carrier)
:
Introspection.SeededLineProgram.axisRepresentativeProg.toFun
((Cost.unary k, Cost.unary j, (SAT.shoupBinField k hk).toBits s), (SAT.shoupBinField k hk).vecBits u) = (SAT.shoupBinField k hk).vecBits
(LIDT.CL.rep (Pi.single (LIDT.CL.chi ⋯ ((ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) s)) 1) u)
The seed change is the same permutation used to prove the exact existing QLD sampled law, so the executable axis stage computes its actual line map.
theorem
MIPRE.QLD.PauliCL.diagonalRepresentativeProg_legacy
(k : ℕ)
(hk : 1 ≤ k)
(j : ℕ)
(hj : j ≤ k)
(s : (SAT.shoupBinField k hk).carrier)
(u v : Fin (2 ^ j) → (SAT.shoupBinField k hk).carrier)
:
have i := LIDT.CL.chi ⋯ ((ExplicitSeed.seedPermutation (SAT.shoupBinField k hk)) s);
have v' := LIDT.CL.zeroBelow i v;
Introspection.SeededLineProgram.diagonalRepresentativeProg.toFun
((Cost.unary k, Cost.unary j, (SAT.shoupBinField k hk).toBits s), (SAT.shoupBinField k hk).vecBits u, (SAT.shoupBinField k hk).vecBits v) = ((SAT.shoupBinField k hk).vecBits (LIDT.CL.rep v' u), (SAT.shoupBinField k hk).vecBits v')
This includes the all-zero selected direction: the point then remains unchanged, exactly as in the existing QLD diagonal sampler.