Uniform binary matrix inversion

def MIPRE.LowDegree.BinaryLinear.matrixSolution {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) (v : Fin m → ZMod 2) : Fin n → ZMod 2

The coefficient vector selected by the deterministic elimination algorithm.

Equations

• MIPRE.LowDegree.BinaryLinear.matrixSolution A v = (MIPRE.LowDegree.BinaryLinear.typedReduce (MIPRE.LowDegree.BinaryLinear.typedBasis (MIPRE.LowDegree.BinaryLinear.columnRows A)) (v, 0)).2

theorem MIPRE.LowDegree.BinaryLinear.matrixSolveProg_encoding {m n : ℕ} (A : Matrix (Fin m) (Fin n) (ZMod 2)) (v : Fin m → ZMod 2) : matrixSolveProg.toFun (Cost.unary n, matrixBits A, vectorBits v) = vectorBits (matrixSolution A v)

theorem MIPRE.LowDegree.BinaryLinear.matrixSolution_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 (matrixSolution A v) = v

def MIPRE.LowDegree.BinaryLinear.inverseMatrix {n : ℕ} (A : Matrix (Fin n) (Fin n) (ZMod 2)) : Matrix (Fin n) (Fin n) (ZMod 2)

The inverse is assembled column by column, solving for each standard basis vector.

Equations

• MIPRE.LowDegree.BinaryLinear.inverseMatrix A i j = MIPRE.LowDegree.BinaryLinear.matrixSolution A (Pi.single j 1) i

theorem MIPRE.LowDegree.BinaryLinear.mul_inverseMatrix {n : ℕ} (A : Matrix (Fin n) (Fin n) (ZMod 2)) (hA : Function.Surjective A.mulVec) : A * inverseMatrix A = 1

For nonsingular matrices, the computed columns form a right inverse.

theorem MIPRE.LowDegree.BinaryLinear.inverseMatrix_mul {n : ℕ} (A : Matrix (Fin n) (Fin n) (ZMod 2)) (hA : Function.Surjective A.mulVec) : inverseMatrix A * A = 1

Over the finite binary field the computed right inverse is also a left inverse.

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

Equations

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

theorem MIPRE.LowDegree.BinaryLinear.inverseColumnsProg_encoding {n : ℕ} (A : Matrix (Fin n) (Fin n) (ZMod 2)) : inverseColumnsProg.toFun (Cost.unary n, matrixBits A) = matrixBits (inverseMatrix A).transpose

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

One globally polynomial-time ambient program for binary matrix inversion. The dimension is explicit and unary; correctness requires a nonsingular matrix.

Equations

• MIPRE.LowDegree.BinaryLinear.inverseMatrixProg = MIPRE.LowDegree.BinaryLinear.transposeBitsProg.comp (MIPRE.Cost.PolyTimeFun.fst.pair MIPRE.LowDegree.BinaryLinear.inverseColumnsProg)

theorem MIPRE.LowDegree.BinaryLinear.inverseMatrixProg_encoding {n : ℕ} (A : Matrix (Fin n) (Fin n) (ZMod 2)) : inverseMatrixProg.toFun (Cost.unary n, matrixBits A) = matrixBits (inverseMatrix A)

The raw program prints canonical coordinates of the constructed inverse matrix.

theorem MIPRE.LowDegree.BinaryLinear.inverseMatrixProg_correct {n : ℕ} (A : Matrix (Fin n) (Fin n) (ZMod 2)) (hA : Function.Surjective A.mulVec) : mulBits n (matrixBits A) (inverseMatrixProg.toFun (Cost.unary n, matrixBits A)) = identityBits n ∧ mulBits n (inverseMatrixProg.toFun (Cost.unary n, matrixBits A)) (matrixBits A) = identityBits n

The printed matrix passes both executable multiplication checks.