A kernel vector by elimination

Let A be a matrix with r rows and n columns over a field. Gaussian elimination finds a nonzero vector v with A v = 0 whenever one exists. This module records a branch-free variant that suits circuits: it maintains n vectors N i spanning the common kernel of the rows processed so far, starting from the unit vectors. To process a row a it computes the values b i = a ⬝ N i, takes the first index j with b j ≠ 0 (the pivot), and replaces each N i by N i - (b i / b j) • N j. The new vectors are killed by a, and every vector of the old span killed by a lies in their span (Cslib.LinearAlgebra.kernelStep). When b = 0 no pivot exists; the pivot value and pivot vector are then zero, and since division by zero is zero in a field the update leaves N unchanged. After all rows the vectors span the kernel of A (Cslib.LinearAlgebra.kernelBasis), and the first nonzero one is the output (Cslib.LinearAlgebra.kernelVec): it lies in the kernel (Cslib.LinearAlgebra.mulVec_kernelVec) and it is nonzero whenever the kernel is (Cslib.LinearAlgebra.kernelVec_ne_zero).

Pivots are selected by the indicator Cslib.LinearAlgebra.firstFlags b of the first nonzero entry of b, so every step is a fixed arithmetic expression in the entries, with tests for zero and no other branching. Processing a row costs O(n ^ 2) field operations. The procedure is Gaussian elimination organized for straight-line evaluation, as needed to count its gates in circuits.

Main definitions

• Cslib.LinearAlgebra.firstFlags: the indicator of the first nonzero entry.
• Cslib.LinearAlgebra.firstNonzero: the first nonzero entry of a vector, as a value.
• Cslib.LinearAlgebra.rowValues: the values a ⬝ N i of a row on the vectors of the family.
• Cslib.LinearAlgebra.pivotVec: the pivot vector, the member of the family at the first nonzero row value, or zero.
• Cslib.LinearAlgebra.kernelStep: process one row.
• Cslib.LinearAlgebra.kernelBasisUpTo: process the first k rows, starting from the unit vectors.
• Cslib.LinearAlgebra.kernelBasis: process all rows, starting from the unit vectors.
• Cslib.LinearAlgebra.kernelVec: the first nonzero vector of the final family.

Main results

• Cslib.LinearAlgebra.mulVec_kernelVec: the output lies in the kernel.
• Cslib.LinearAlgebra.kernelVec_ne_zero: the output is nonzero when the kernel is nontrivial.

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]

The first nonzero entry

def Cslib.LinearAlgebra.firstFlags {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (b : Fin n → F) (i : Fin n) : F

firstFlags b i is one at the first index i with b i ≠ 0 and zero elsewhere; it is zero everywhere when b = 0.

theorem Cslib.LinearAlgebra.firstFlags_of_eq_zero {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} {b : Fin n → F} (hb : b = 0) : firstFlags b = 0

The flags of the zero vector are zero.

theorem Cslib.LinearAlgebra.exists_firstFlags_eq_single {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} {b : Fin n → F} (hb : b ≠ 0) : ∃ (j : Fin n), b j ≠ 0 ∧ (∀ i < j, b i = 0) ∧ firstFlags b = Pi.single j 1

For b ≠ 0, firstFlags b is the indicator of the first index j with b j ≠ 0.

theorem Cslib.LinearAlgebra.sum_firstFlags_smul_eq {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} {M : Type u_2} [AddCommMonoid M] [Module F M] (b : Fin n → F) (g : Fin n → M) : b = 0 ∧ ∑ i : Fin n, firstFlags b i • g i = 0 ∨ ∃ (j : Fin n), b j ≠ 0 ∧ (∀ i < j, b i = 0) ∧ ∑ i : Fin n, firstFlags b i • g i = g j

Weighting a family by firstFlags b selects its member at the first nonzero entry of b, or gives zero when b = 0.

The first nonzero entry as a value

def Cslib.LinearAlgebra.firstNonzero {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (u : Fin n → F) : F

The first nonzero entry of a vector, or zero for the zero vector.

theorem Cslib.LinearAlgebra.firstNonzero_eq_zero_iff {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} {u : Fin n → F} : firstNonzero u = 0 ↔ u = 0

The first nonzero entry vanishes only for the zero vector.

theorem Cslib.LinearAlgebra.firstNonzero_smul {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (c : F) (u : Fin n → F) : firstNonzero (c • u) = c * firstNonzero u

Scaling a vector scales its first nonzero entry.

theorem Cslib.LinearAlgebra.firstNonzero_smul_inv_smul {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} {u : Fin n → F} (hu : u ≠ 0) : firstNonzero u • (firstNonzero u)⁻¹ • u = u

A nonzero vector u is firstNonzero u times its normalization (firstNonzero u)⁻¹ • u.

Elimination

def Cslib.LinearAlgebra.rowValues {F : Type u_1} [Field F] {n : ℕ} (a : Fin n → F) (N : Fin n → Fin n → F) (i : Fin n) : F

The values a ⬝ N i of the row a on the vectors of the family.

def Cslib.LinearAlgebra.pivotVec {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (a : Fin n → F) (N : Fin n → Fin n → F) : Fin n → F

The pivot vector: the member of the family at the first nonzero row value, or zero.

def Cslib.LinearAlgebra.kernelStep {F : Type u_1} [Field F] [DecidableEq F] {n : ℕ} (a : Fin n → F) (N : Fin n → Fin n → F) (i : Fin n) : Fin n → F

One elimination step. Replace each vector N i of the family by N i - (b i / β) • P, where b are the row values, P the pivot vector and β = a ⬝ P the pivot value.

def Cslib.LinearAlgebra.kernelBasisUpTo {F : Type u_1} [Field F] [DecidableEq F] {n r : ℕ} (A : Matrix (Fin r) (Fin n) F) : ℕ → Fin n → Fin n → F

The family after processing the first k rows of A, starting from the unit vectors.

def Cslib.LinearAlgebra.kernelBasis {F : Type u_1} [Field F] [DecidableEq F] {n r : ℕ} (A : Matrix (Fin r) (Fin n) F) : Fin n → Fin n → F

The family after processing all rows of A; its span is the kernel of A.

def Cslib.LinearAlgebra.kernelVec {F : Type u_1} [Field F] [DecidableEq F] {n r : ℕ} (A : Matrix (Fin r) (Fin n) F) : Fin n → F

A kernel vector. The first nonzero vector of kernelBasis A, or zero if all of them are zero.

Correctness

theorem Cslib.LinearAlgebra.mulVec_kernelVec {F : Type u_1} [Field F] [DecidableEq F] {n r : ℕ} (A : Matrix (Fin r) (Fin n) F) : A.mulVec (kernelVec A) = 0

The kernel vector lies in the kernel.

theorem Cslib.LinearAlgebra.kernelVec_ne_zero {F : Type u_1} [Field F] [DecidableEq F] {n r : ℕ} (A : Matrix (Fin r) (Fin n) F) (h : ∃ (v : Fin n → F), v ≠ 0 ∧ A.mulVec v = 0) : kernelVec A ≠ 0

The kernel vector is nonzero when the kernel is nontrivial.