Kernel generators of a register-local linear map, as the image of a program #

The constraint families of MIPRE.Tailored.Intro.AuxCons are parametric in lists of generators of the kernels of register-local linear maps (KerGens). This file supplies one, as the image of a single polynomial-time program.

The program is the existing binary kernel solver LowDegree.BinaryLinear.kernelGeneratorsProg: it eliminates the columns of the matrix together with an identity certificate and prints the reduced certificate of each standard basis vector, that is the images of the standard basis under a projection onto the kernel. Here its correctness is restated in the coordinates of the sampler (CL.toBits, CL.ofBits):

kernelGens: the program, on the column count s in unary and the rows of the matrix;
kernelGens_correct: for A : Matrix (Fin m) (Fin s) 𝔽₂ given by its rows, every output vector has length s and lies in the kernel of A, and every kernel vector is in their span;
regKerGens, kerGens_regKerGens: for a register-local map M on 𝔽₂^Q, the program run on the rows of the matrix of M gives generators of the kernel of M, so regKerGens satisfies KerGens Q.

source

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.kernelGens :

Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr) (List Cost.BitStr)

Generators of the kernel of an m × s binary matrix, computed in polynomial time from s in unary and the matrix rows as bit strings of length s.

Equations

MIPRE.Tailored.Intro.kernelGens = MIPRE.LowDegree.BinaryLinear.kernelGeneratorsProg

Instances For

source

theorem MIPRE.Tailored.Intro.vectorBits_eq_toBits {s : ℕ} (v : Fin s → CL.𝔽₂) :

LowDegree.BinaryLinear.vectorBits v = CL.toBits v

source

theorem MIPRE.Tailored.Intro.vectorValue_eq_ofBits (s : ℕ) (l : Cost.BitStr) :

LowDegree.BinaryLinear.vectorValue s l = CL.ofBits s l

source

theorem MIPRE.Tailored.Intro.matrixBits_eq {m s : ℕ} (A : Matrix (Fin m) (Fin s) CL.𝔽₂) :

LowDegree.BinaryLinear.matrixBits A = List.ofFn fun (i : Fin m) => CL.toBits (A i)

source

theorem MIPRE.Tailored.Intro.kernelGens_correct {m s : ℕ} (A : Matrix (Fin m) (Fin s) CL.𝔽₂) :

(∀ v ∈ kernelGens.toFun (Cost.unary s, List.ofFn fun (i : Fin m) => CL.toBits (A i)), List.length v = s ∧ A.mulVec (CL.ofBits s v) = 0) ∧ ∀ (z : Fin s → CL.𝔽₂), A.mulVec z = 0 → z ∈ Submodule.span CL.𝔽₂ {x : Fin s → CL.𝔽₂ | ∃ v ∈ kernelGens.toFun (Cost.unary s, List.ofFn fun (i : Fin m) => CL.toBits (A i)), CL.ofBits s v = x}

The kernel generators program is correct. Every output vector has length s and lies in the kernel of A; every vector of the kernel is in the span of the outputs.

source