2.1. Introduction🔗

Released as hex-row-reduce, with the Mathlib correspondence in hex-row-reduce-mathlib.

HexRowReduce does Gauss-Jordan reduction of a matrix over a field to reduced row echelon form, and computes the row span and nullspace from it. It depends only on HexMatrix.

The reduction returns a certificate, not just a reduced matrix: the rank, the reduced form, an invertible transform T with T * original = echelon, and the pivot columns. The span and nullspace operations are computed from it, each proved correct for the original matrix M by a soundness theorem (the nullspace basis also has a completeness theorem).

HexRowReduce is Mathlib-free. HexRowReduceMathlib identifies its rank, span, and nullspace with their Mathlib analogues Matrix.rank, Submodule.span, and LinearMap.ker. The proof recipes below use it.