Inverse Matrix Rigidity: Exact Formula and Optimal Positions for Minimum Rank Restoration

This paper introduces inverse matrix rigidity R(A): the minimum number of entries that must be modified to convert a singular matrix A ∈ Kⁿˣⁿ into an invertible matrix, over any field K. The main theorem establishes the exact formula R(A) = n − rank(A) = nullity(A). The proof combines a rank-subadditivity lower bound with a constructive upper bound using a maximum nonsingular minor and a multilinear polynomial argument. The paper also develops optimal position identification, a rectangular extension, restricted-support analysis via bipartite matching, robust rank restoration with singular-value guarantees, and applications to observability, electrical networks, and mechanical metamaterials. A Lean 4 formal verification (329 lines, 0 errors) is available at DOI: 10.5281/zenodo.21080257. A Python GUI companion is available at DOI: 10.5281/zenodo.21083715.