Echelon-form data and contracts.

RowEchelonData is the pure result of an echelon-form algorithm (rank, echelon matrix, accumulated transform, pivot columns). IsEchelonForm is the shared contract for any echelon form; IsRowReduced extends it with the reduced-row-echelon conditions (pivots are one, entries above pivots vanish). The IsEchelonForm namespace lemmas develop the pivot/free-column partition used by the span and nullspace APIs.

structure Hex.Matrix.RowEchelonData (R : Type u) (n m : Nat) : Type u

Pure data produced by an echelon-form algorithm.

• rank : Nat

  Number of pivots, i.e. the rank of the original matrix.

• echelon : Matrix R n m

  The matrix reduced to row-echelon form.

• transform : Matrix R n n

  The accumulated row-operation transform T with T * original = echelon.

• pivotCols : Vector (Fin m) self.rank

  Column index of each pivot, in increasing order.

structure Hex.Matrix.IsEchelonForm {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] (M : Matrix R n m) (D : RowEchelonData R n m) : Prop

Shared conditions for any echelon form.

• transform_mul : D.transform * M = D.echelon
• transform_inv : ∃ (Tinv : Matrix R n n), Tinv * D.transform = Matrix.identity n
• transform_right_inv : ∃ (Tinv : Matrix R n n), D.transform * Tinv = Matrix.identity n
• rank_le_n : D.rank ≤ n
• rank_le_m : D.rank ≤ m
• pivotCols_sorted (i j : Fin D.rank) : i < j → D.pivotCols.get i < D.pivotCols.get j
• below_pivot_zero (i : Fin D.rank) (j : Fin n) : ↑i < ↑j → D.echelon[j][D.pivotCols.get i] = 0
• zero_row (i : Fin n) : D.rank ≤ ↑i → D.echelon[i] = 0

structure Hex.Matrix.IsRowReduced {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] (M : Matrix R n m) (D : RowEchelonData R n m) extends M.IsEchelonForm D : Prop

RREF-specific conditions on top of IsEchelonForm.

• transform_mul : D.transform * M = D.echelon
• transform_inv : ∃ (Tinv : Matrix R n n), Tinv * D.transform = Matrix.identity n
• transform_right_inv : ∃ (Tinv : Matrix R n n), D.transform * Tinv = Matrix.identity n
• rank_le_n : D.rank ≤ n
• rank_le_m : D.rank ≤ m
• pivotCols_sorted (i j : Fin D.rank) : i < j → D.pivotCols.get i < D.pivotCols.get j
• below_pivot_zero (i : Fin D.rank) (j : Fin n) : ↑i < ↑j → D.echelon[j][D.pivotCols.get i] = 0
• zero_row (i : Fin n) : D.rank ≤ ↑i → D.echelon[i] = 0
• pivot_one (i : Fin D.rank) : D.echelon[i][D.pivotCols.get i] = 1
• above_pivot_zero (i : Fin D.rank) (j : Fin n) : ↑j < ↑i → D.echelon[j][D.pivotCols.get i] = 0

def Hex.Matrix.IsEchelonForm.pivotRow {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsEchelonForm D) (i : Fin D.rank) : Fin n

View a pivot-row index as a row index of the ambient matrix.

Equations

• E.pivotRow i = ⟨↑i, ⋯⟩

def Hex.Matrix.IsEchelonForm.HasNonzeroPivots {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsEchelonForm D) : Prop

The pivot entries named by pivotCols are nonzero. This is the extra proof-facing contract needed by span solving: without it, the pivot-column division in spanCoeffs can divide by zero.

Equations

• E.HasNonzeroPivots = ∀ (i : Fin D.rank), D.echelon[E.pivotRow i][D.pivotCols.get i] ≠ 0

theorem Hex.Matrix.IsEchelonForm.transform_mul_inv {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsEchelonForm D) : ∃ (Tinv : Matrix R n n), D.transform * Tinv = Matrix.identity n

The square row-transform has a right inverse.

theorem Hex.Matrix.IsEchelonForm.pivotCols_injective {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsEchelonForm D) : Function.Injective fun (i : Fin D.rank) => D.pivotCols.get i

The pivot columns are injective because they are strictly increasing.

def Hex.Matrix.IsEchelonForm.freeColsList {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} (_E : M.IsEchelonForm D) : List (Fin m)

The non-pivot columns, enumerated in increasing order.

The echelon-form witness _E is a phantom argument: it carries no runtime data but enables dot-notation (E.freeColsList) and fixes the implicit matrix/data parameters. This intentionally triggers the unusedArguments linter; the binder is kept deliberately (no @[nolint] exists in the Mathlib-free layer).

Equations

• _E.freeColsList = List.filter (fun (j : Fin m) => decide ¬j ∈ D.pivotCols.toList) (List.finRange m)

theorem Hex.Matrix.IsEchelonForm.freeColsList_length {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsEchelonForm D) : E.freeColsList.length = m - D.rank

The number of free columns is the ambient column count minus the rank.

def Hex.Matrix.IsEchelonForm.freeCols {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsEchelonForm D) : Vector (Fin m) (m - D.rank)

Sorted complement of the pivot columns.

Equations

• E.freeCols = Vector.mk E.freeColsList.toArray ⋯

theorem Hex.Matrix.IsEchelonForm.freeCols_sorted {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsEchelonForm D) (i j : Fin (m - D.rank)) : i < j → E.freeCols.get i < E.freeCols.get j

The free-column complement is strictly increasing.

theorem Hex.Matrix.IsEchelonForm.freeCols_injective {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsEchelonForm D) : Function.Injective fun (i : Fin (m - D.rank)) => E.freeCols.get i

The free columns are injective because they are strictly increasing.

theorem Hex.Matrix.IsEchelonForm.colPartition {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsEchelonForm D) (j : Fin m) : (∃ (i : Fin D.rank), D.pivotCols.get i = j) ∨ ∃ (k : Fin (m - D.rank)), E.freeCols.get k = j

Every column is either a pivot column or a free column.

theorem Hex.Matrix.IsEchelonForm.colPartition_exclusive {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsEchelonForm D) (j : Fin m) : ¬((∃ (i : Fin D.rank), D.pivotCols.get i = j) ∧ ∃ (k : Fin (m - D.rank)), E.freeCols.get k = j)

No column can simultaneously occur in the pivot list and the free-column complement.

theorem Hex.Matrix.IsEchelonForm.pivotCols_disjoint_freeCols {R : Type u_1} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsEchelonForm D) (i : Fin D.rank) (k : Fin (m - D.rank)) : D.pivotCols.get i ≠ E.freeCols.get k

No column can be both pivot and free.