Circuits for kernel vectors

The elimination procedure Cslib.LinearAlgebra.kernelVec, which returns a nonzero vector in the kernel of a matrix whenever there is one, is a fixed arithmetic computation with tests for zero. Over the full binary basis of a field, where every operation on at most two field elements is one gate, it costs O((r + 1) * n ^ 2) gates for a matrix with r rows and n columns: the indicator of the first nonzero entry of a vector of length n costs 2 * n + 1 gates (Cslib.Circuits.Synthesis.full_firstFlags), one elimination step at most 8 * (n + 1) ^ 2 (Cslib.Circuits.Synthesis.full_kernelStep) and the whole procedure at most kernelVecCost r n = 8 * (r + 1) * (n + 1) ^ 2 (Cslib.Circuits.Synthesis.full_kernelVec). The entries of the matrix may be arbitrary available functions of the circuit's inputs.

Main definitions

• Cslib.Circuits.kernelVecCost: the gate budget of the elimination procedure.

Main results

• Cslib.Circuits.Synthesis.full_firstFlags: the first nonzero entry.
• Cslib.Circuits.Synthesis.full_nonzero: the indicator of a nonzero vector.
• Cslib.Circuits.Synthesis.full_kernelStep: one elimination step.
• Cslib.Circuits.Synthesis.full_kernelVec: a kernel vector.

References

• [P. Bürgisser, M. Clausen, M. A. Shokrollahi, Algebraic Complexity Theory] [BCS97]
• [M. Sudan, L. Trevisan, S. Vadhan, Pseudorandom generators without the XOR lemma] [STV01]

def Cslib.Circuits.kernelVecCost (r n : ℕ) : ℕ

The gate budget of the elimination procedure for r rows and n columns over the full binary basis.

theorem Cslib.Circuits.Synthesis.full_firstFlags {F : Type u_1} [Field F] [DecidableEq F] {N n : ℕ} {s : Set ((Fin N → F) → F)} (b : Fin n → (Fin N → F) → F) (hb : ∀ (i : Fin n), b i ∈ s) : Synthesis fullInterpretation s (Set.range fun (i : Fin n) (x : Fin N → F) => LinearAlgebra.firstFlags (fun (j : Fin n) => b j x) i) (2 * n + 1)

The first nonzero entry. The indicators firstFlags b i of the first nonzero entry of a vector of n available functions cost 2 * n + 1 gates of the full binary basis.

theorem Cslib.Circuits.Synthesis.full_nonzero {F : Type u_1} [Field F] [DecidableEq F] {N n : ℕ} {s : Set ((Fin N → F) → F)} (v : Fin n → (Fin N → F) → F) (hv : ∀ (l : Fin n), v l ∈ s) : Synthesis fullInterpretation s {fun (x : Fin N → F) => if (fun (l : Fin n) => v l x) = 0 then 0 else 1} (n + 1)

The indicator that a vector of n available functions is nonzero costs n + 1 gates of the full binary basis.

theorem Cslib.Circuits.Synthesis.full_kernelStep {F : Type u_1} [Field F] [DecidableEq F] {N n : ℕ} {s : Set ((Fin N → F) → F)} (a : Fin n → (Fin N → F) → F) (Nv : Fin n → Fin n → (Fin N → F) → F) (ha : ∀ (l : Fin n), a l ∈ s) (hN : ∀ (i l : Fin n), Nv i l ∈ s) : Synthesis fullInterpretation s (Set.range fun (il : Fin n × Fin n) (x : Fin N → F) => LinearAlgebra.kernelStep (fun (l : Fin n) => a l x) (fun (i l : Fin n) => Nv i l x) il.1 il.2) (8 * (n + 1) ^ 2)

One elimination step. If the entries of the row a and of the family Nv are available, the entries of kernelStep a Nv cost at most 8 * (n + 1) ^ 2 gates of the full binary basis.

theorem Cslib.Circuits.Synthesis.full_kernelVec {F : Type u_1} [Field F] [DecidableEq F] {N n r : ℕ} {s : Set ((Fin N → F) → F)} (A : Fin r → Fin n → (Fin N → F) → F) (hA : ∀ (k : Fin r) (l : Fin n), A k l ∈ s) : Synthesis fullInterpretation s (Set.range fun (l : Fin n) (x : Fin N → F) => LinearAlgebra.kernelVec (fun (k : Fin r) (l : Fin n) => A k l x) l) (kernelVecCost r n)

A kernel vector by a circuit. If the entries of a matrix with r rows and n columns are available, the entries of kernelVec A cost at most kernelVecCost r n = 8 * (r + 1) * (n + 1) ^ 2 gates of the full binary basis.