def Hex.Matrix.Retained.loop {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} (col fuel : Nat) (state : RowReduceState F n m) (W : Matrix F n n) : RowReduceState F n m × Matrix F n n

Carry the inverse transform alongside the existing Gauss-Jordan steps. The state projection uses exactly the ordinary elimination operation.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.Retained.loop col 0 state W = (state, W)

theorem Hex.Matrix.Retained.loop_fst {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} (col fuel : Nat) (state : RowReduceState F n m) (W : Matrix F n n) : (loop col fuel state W).fst = rowReduceLoop col fuel state

Retaining inverse operations leaves the executable RREF unchanged.

def Hex.Matrix.Retained.data {F : Type u} {n m : Nat} (state : RowReduceState F n m) : RowEchelonData F n m

Package the ordinary final state without recomputing it.

Equations

• Hex.Matrix.Retained.data state = { rank := state.pivots.length, echelon := state.echelon, transform := state.transform, pivotCols := Vector.mk state.pivots.toArray ⋯ }

def Hex.Matrix.Retained.reduce {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} (A : Matrix F n m) : RowEchelonData F n m × Matrix F n n

One reduction, retaining the inverse transform for a complete certificate.

Equations

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

theorem Hex.Matrix.Retained.reduce_fst {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n m : Nat} (A : Matrix F n m) : (reduce A).fst = A.rowReduce

def Hex.Matrix.inverseWitness {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (toRat : F → Rat) {n : Nat} (A : Matrix F n n) : InverseWitness

Produce either an inverse or a nonzero nullspace column from one RREF.

Equations

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

def Hex.Matrix.solveWitness {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (toRat : F → Rat) {n m : Nat} (A : Matrix F n m) (b : Vector F n) : SolveWitness

Produce complete affine data or a separator, retaining the inverse transform without repeating elimination. The solving step is shared with solve.

Equations

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