Correctness of the Gauss-Jordan rowReduceLoop for hex-matrix.

This module runs rowReduceLoop to a finished rowReduce and proves it meets the IsRowReduced contract. It tracks the loop's proof-only invariants through each pivot step: the shape invariant (rowReduceLoop_shape), the canonical-column invariant (rowReduceLoop_canonical), the no-pivot-zero invariant (rowReduceLoop_no_pivot_zero), the same-operation transform equation (rowReduceLoop_transform_preserve), and existence of left/right inverses for the transform, then specializes each to the full run. The headline def rowReduce packages the result, with rowReduce_isRowReduced assembling the IsEchelonForm/IsRowReduced fields and rowReduce_transform_mul, rowReduce_rank_le_n, rowReduce_pivotCols_sorted exposing the wrapper-level projections.

def Hex.Matrix.rowReduce {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : RowEchelonData R n m

Reduced row echelon form data computed by Gauss-Jordan elimination.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.Matrix.rowReduce_rank_le_n {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : M.rowReduce.rank ≤ n

Wrapper-level projection of the rank row bound from rowReduce_isRowReduced M.

theorem Hex.Matrix.rowReduce_rank_le_m {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : M.rowReduce.rank ≤ m

Wrapper-level projection of the rank column bound from rowReduce_isRowReduced M.

theorem Hex.Matrix.rowReduce_pivotCols_sorted {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) (i j : Fin M.rowReduce.rank) : i < j → M.rowReduce.pivotCols.get i < M.rowReduce.pivotCols.get j

Wrapper-level projection of pivot-column sortedness from rowReduce_isRowReduced M.

theorem Hex.Matrix.rowReduce_transform_mul {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : M.rowReduce.transform * M = M.rowReduce.echelon

Wrapper-level projection of the transform equation from rowReduce_isRowReduced M.

theorem Hex.Matrix.rowReduce_isRowReduced {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (M : Matrix R n m) : M.IsRowReduced M.rowReduce

The computed rowReduce data satisfies the IsRowReduced contract.