A uniform solver for binary matrices

def MIPRE.LowDegree.BinaryLinear.unitBits (n j : ℕ) : Cost.BitStr

Equations

• MIPRE.LowDegree.BinaryLinear.unitBits n j = List.map (fun (i : ℕ) => decide (i = j)) (List.range n)

def MIPRE.LowDegree.BinaryLinear.identityBits (n : ℕ) : List Cost.BitStr

Equations

• MIPRE.LowDegree.BinaryLinear.identityBits n = List.map (MIPRE.LowDegree.BinaryLinear.unitBits n) (List.range n)

theorem MIPRE.LowDegree.BinaryLinear.unitBits_eq_vectorBits {n : ℕ} (j : Fin n) : unitBits n ↑j = vectorBits (Pi.single j 1)

theorem MIPRE.LowDegree.BinaryLinear.identityBits_eq_matrixBits (n : ℕ) : identityBits n = matrixBits 1

noncomputable def MIPRE.LowDegree.BinaryLinear.unitBitsProg : Cost.PolyTimeFun (ℕ × Cost.Unary) Cost.BitStr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LowDegree.BinaryLinear.identityBitsProg : Cost.PolyTimeFun Cost.Unary (List Cost.BitStr)

Equations

• One or more equations did not get rendered due to their size.

def MIPRE.LowDegree.BinaryLinear.coordinateRows (columns : List Cost.BitStr) : List RawRow

Attach the standard coordinate certificate to each supplied column.

Equations

• MIPRE.LowDegree.BinaryLinear.coordinateRows columns = columns.zip (MIPRE.LowDegree.BinaryLinear.identityBits columns.length)

noncomputable def MIPRE.LowDegree.BinaryLinear.coordinateRowsProg : Cost.PolyTimeFun (List Cost.BitStr) (List RawRow)

Equations

• One or more equations did not get rendered due to their size.

def MIPRE.LowDegree.BinaryLinear.columnRows {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) : List (Row m n)

Equations

• MIPRE.LowDegree.BinaryLinear.columnRows A = List.ofFn fun (j : Fin n) => (A.col j, Pi.single j 1)

theorem MIPRE.LowDegree.BinaryLinear.coordinateRows_matrixBits {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) : coordinateRows (transposeBits n (matrixBits A)) = List.map rowBits (columnRows A)

theorem MIPRE.LowDegree.BinaryLinear.columnRows_represents {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) (r : Row m n) : r ∈ columnRows A → Represents A.mulVecLin r

theorem MIPRE.LowDegree.BinaryLinear.rowSpan_columnRows {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) : rowSpan (columnRows A) = A.mulVecLin.range

noncomputable def MIPRE.LowDegree.BinaryLinear.matrixSolveProg : Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr × Cost.BitStr) Cost.BitStr

The output width is unary; matrix rows and the right-hand side are raw bits.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LowDegree.BinaryLinear.matrixSolveProg_correct {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) (v : Fin m → ZMod 2) (hv : ∃ (x : Fin n → ZMod 2), A.mulVec x = v) : A.mulVec (vectorValue n (matrixSolveProg.toFun (Cost.unary n, matrixBits A, vectorBits v))) = v

A globally polynomial-time solver for every consistent binary matrix system.

noncomputable def MIPRE.LowDegree.BinaryLinear.addMatrixBitsProg : Cost.PolyTimeFun (List Cost.BitStr × List Cost.BitStr) (List Cost.BitStr)

Coordinatewise addition of binary matrices.

Equations

• MIPRE.LowDegree.BinaryLinear.addMatrixBitsProg = MIPRE.LowDegree.BinaryPolynomial.xorBitsProg.map.comp MIPRE.Cost.PolyTimeFun.zip

theorem MIPRE.LowDegree.BinaryLinear.addMatrixBitsProg_correct {m n : ℕ} (A B : Matrix (Fin m) (Fin n) (ZMod 2)) : addMatrixBitsProg.toFun (matrixBits A, matrixBits B) = matrixBits (A + B)