Rank, row-span, and nullspace correspondence theorems for hex-matrix-mathlib.

This module converts the executable Hex.Matrix row-reduction data into Mathlib's function-based matrix model, then states theorems relating computed rank, span membership, and nullspace bases to Mathlib's noncomputable linear-algebra definitions.

theorem HexMatrixMathlib.vectorEquiv_vecMul {R : Type u} {n m : ℕ} [CommRing R] (M : Hex.Matrix R n m) (c : Vector R n) : vectorEquiv (Hex.Matrix.vecMul c M) = (Fintype.linearCombination R (matrixEquiv M).row) (vectorEquiv c)

The executable row combination Hex.Matrix.vecMul c M (the linear combination of the rows of M with coefficients c) transports under vectorEquiv to Mathlib's Fintype.linearCombination over the rows of matrixEquiv M. This identifies the computed row span with Mathlib's span.

theorem HexMatrixMathlib.spanCoeffs_eq_linearCombination {R : Type u} {n m : ℕ} [Field R] [DecidableEq R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m} (E : M.IsEchelonForm D) (v : Vector R m) (c : Vector R n) : E.spanCoeffs v = some c → vectorEquiv v = (Fintype.linearCombination R (matrixEquiv M).row) (vectorEquiv c)

Soundness of the executable spanCoeffs: when echelon-form data certifies v as a row combination with coefficients c, the Mathlib image of v is the corresponding linearCombination of the rows of M. Witnesses span membership with explicit coefficients.

theorem HexMatrixMathlib.spanContains_iff_mem_span {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 ↔ vectorEquiv v ∈ Submodule.span R (Set.range (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.rowReduce_echelon_row_mem_span {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) (i : Fin n) : vectorEquiv (D.echelon.row i) ∈ Submodule.span R (Set.range (matrixEquiv M).row)

Every row of the computed echelon form lies in the row span of the original matrix M: row reduction does not enlarge the span. One inclusion of the "echelon rows span the same subspace as M" equivalence.

theorem HexMatrixMathlib.rowReduce_mem_span_echelon_of_mem_span {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 : Fin m → R} : v ∈ Submodule.span R (Set.range (matrixEquiv M).row) → ∃ (c : Vector R n), Hex.Matrix.vecMul c D.echelon = vectorEquiv.symm v

Converse direction: any vector in the row span of M is realised as an executable row combination of the echelon rows. Together with rowReduce_echelon_row_mem_span this shows row reduction preserves the row span.

theorem HexMatrixMathlib.nullspace_mem_ker {R : Type u} {n m : ℕ} [Field R] {M : Hex.Matrix R n m} {D : Hex.Matrix.RowEchelonData R n m} (E : M.IsRowReduced D) (k : Fin (m - D.rank)) : vectorEquiv (E.nullspace.get k) ∈ (matrixEquiv M).mulVecLin.ker

Each computed nullspace basis vector lies in the kernel of M (viewed as Mathlib's linear map mulVecLin): the executable nullspace really annihilates M.

theorem HexMatrixMathlib.nullspace_span_eq_ker {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 : Fin (m - D.rank)) => vectorEquiv (E.nullspace.get k)) = (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.

theorem HexMatrixMathlib.rank_eq {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 = (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.