On matrix rank function over bounded arithmetics

TL;DR

This paper formalizes Mulmuley's matrix rank algorithm within bounded arithmetic, showing that properties of determinants imply rank equivalences, and demonstrates the formalization's capability in a logical theory with applications to combinatorics.

Contribution

It formalizes the matrix rank computation and determinant properties in bounded arithmetic, connecting algebraic algorithms with logical theories.

Findings

Formalization of rank and determinant properties in bounded arithmetic.

Proof that determinant multiplicativity implies rank equivalence.

Examples of combinatorial statements provable in the formal system.

Abstract

In [Mulmuley, 1987], Mulmuley gave an algorithm reducing the computation of the matrix rank function to that of determinants, of which the proof for the verification is elementary. In this article, we formalize this argument in the bounded arithmetic $LAP$; that is, we show that \[\det(AB)=\det(A)\det(B)\] for matrices $A,B$ with $mathbb{F}(X)$-coefficients implies \[rank(M)=dim(im M),\] where $\mathbb{F}$ is the universe of the field-sort of the theory, $M$ is a matrix with $\mathbb{F}$-coefficients, and $rank(M)$ is the rank function computed by Mulmuley's algorithm. Furthermore, interpreting $LAP$ by $VNC^{2}$ with $\mathbb{F}=\mathbb{Q}$ and using the result of [Tzameret \& Cook, 2021], we see that $VNC^{2}$ can formalize $rank(M)$ and prove $rank(M)=dim(im M)$. Lastly, we give several examples of combinatorial statements provable in $VNC^{2}$, using the formalized linear algebra.