Pivot search and column elimination for the hex-matrix RREF loop.

This module supplies the executable building blocks of Gauss-Jordan elimination and their entrywise lemmas. It defines the RowReduceState carrier, the pivot search findPivot? (with the _some_ge, _some_nonzero, _some_above, _none characterizations) and the column-clearing eliminateColumn, proving the latter zeros non-pivot rows, fixes the pivot row, leaves other columns untouched, and preserves both the transform equation and the transform's left/right inverses. It assembles the rowReduceLoop driver itself together with the proof-only RowReduceShapeInvariant, RowReduceCanonicalInvariant structures and their one-step concat extension lemmas, which RREF/Loop then carries through the recursion.

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

• row : Nat
• echelon : Matrix R n m
• transform : Matrix R n n
• pivots : List (Fin m)

def Hex.Matrix.rowReduceLoop {R : Type u} {n m : Nat} [Lean.Grind.Field R] [DecidableEq R] (col fuel : Nat) (state : RowReduceState R n m) : RowReduceState R n m

Process columns left-to-right, performing Gauss-Jordan elimination.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.rowReduceLoop col 0 state = state