16.5. The Mathlib correspondence🔗

HexRowReduce computes with the length-indexed Hex.Matrix type and stays Mathlib-free. The public HexRowReduceMathlib umbrella transports its certified output through HexMatrixMathlib.matrixEquiv and HexMatrixMathlib.vectorEquiv; users reason with the named theorems below and need not unfold either equivalence or the elimination loop.

The computed rank is exactly Mathlib's matrix rank.

theorem

HexMatrixMathlib.rank_eq.{u} {R : Type u} {n m : ℕ} [Field R]
  {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m}
  (E : M.IsRowReduced D) :
  D.rank = (HexMatrixMathlib.matrixEquiv M).rank
HexMatrixMathlib.rank_eq.{u} {R : Type u}
  {n m : ℕ} [Field R]
  {M : Hex.Matrix R n m}
  {D : Hex.Matrix.RowEchelonData R n m}
  (E : M.IsRowReduced D) :
  D.rank =
    (HexMatrixMathlib.matrixEquiv M).rank

The rank computed by row reduction agrees with Mathlib's Matrix.rank. Proven by rank-nullity: the m - D.rank independent nullspace basis vectors pin the kernel dimension, and the complement is the matrix rank.

The Boolean span test characterizes membership in the Mathlib span of the original rows, while the computed nullspace spans precisely the kernel of Mathlib's mulVec linear map.

theorem

HexMatrixMathlib.spanContains_iff_mem_span.{u} {R : Type u} {n m : ℕ}
  [Field R] [DecidableEq R] {M : Hex.Matrix R n m}
  {D : Hex.Matrix.RowEchelonData R n m} (E : M.IsRowReduced D)
  (v : Vector R m) :
  ⋯.spanContains v = true ↔
    HexMatrixMathlib.vectorEquiv v ∈
      Submodule.span R (Set.range (HexMatrixMathlib.matrixEquiv M).row)
HexMatrixMathlib.spanContains_iff_mem_span.{u}
  {R : Type u} {n m : ℕ} [Field R]
  [DecidableEq R] {M : Hex.Matrix R n m}
  {D : Hex.Matrix.RowEchelonData R n m}
  (E : M.IsRowReduced D)
  (v : Vector R m) :
  ⋯.spanContains v = true ↔
    HexMatrixMathlib.vectorEquiv v ∈
      Submodule.span R
        (Set.range
          (HexMatrixMathlib.matrixEquiv
              M).row)

The executable span-membership test spanContains is correct: it returns true exactly when the Mathlib image of v lies in the R-span of the rows of M. The decision procedure agrees with Mathlib's Submodule.span.

theorem

HexMatrixMathlib.nullspace_span_eq_ker.{u} {R : Type u} {n m : ℕ}
  [Field R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m}
  (E : M.IsRowReduced D) :
  Submodule.span R
      (Set.range fun k =>
        HexMatrixMathlib.vectorEquiv (E.nullspace.get k)) =
    (HexMatrixMathlib.matrixEquiv M).mulVecLin.ker
HexMatrixMathlib.nullspace_span_eq_ker.{u}
  {R : Type u} {n m : ℕ} [Field R]
  {M : Hex.Matrix R n m}
  {D : Hex.Matrix.RowEchelonData R n m}
  (E : M.IsRowReduced D) :
  Submodule.span R
      (Set.range fun k =>
        HexMatrixMathlib.vectorEquiv
          (E.nullspace.get k)) =
    (HexMatrixMathlib.matrixEquiv
          M).mulVecLin.ker

The computed nullspace basis spans exactly the kernel of M: the span of the executable basis vectors equals Mathlib's LinearMap.ker (mulVecLin M). This is the completeness counterpart to nullspace_mem_ker.

These results consume Hex.Matrix.IsRowReduced, the certificate returned by the executable driver. They do not depend on accidental definitional equality between Hex and Mathlib matrices.