In-Place Dense Homogeneous Kernels

A memory-efficient executable variant of the dense Gauss-Jordan homogeneous-kernel backend.

The functions in RowOps.lean and Kernel.lean thread a whole DenseMatrix structure through every row operation. Because scaleRow/addScaledRow/swapRows read the matrix through M.get while the structure M is still live, the backing Array is multiply-referenced at the first setD, so Array.setIfInBounds copies the entire array on every row-operation call. Gauss-Jordan elimination performs Θ(rows) row operations per pivot and Θ(min rows cols) pivots, so the copies turn an O(n³) algorithm into O(n⁴) work plus Θ(n⁴) words of short-lived allocation.

This module performs the same arithmetic, in the same order, threading a bare Array F (with the dimensions carried as separate Nat arguments) through the reduction. The array is uniquely referenced as it flows from one operation to the next, so setIfInBounds mutates in place after at most one fork from a shared input. The reduced matrix and pivot data are bit-for-bit identical to rref, so the extracted witnesses agree with homogeneousWitness.

The free-column witness extraction (freeColumns, basisVectorForFreeColumn) is cheap and shared verbatim with Kernel.lean.

def CompPoly.DenseMatrix.swapRowsData {F : Type u_1} [Zero F] (cols rowA rowB : ℕ) (data : Array F) : Array F

Swap rows rowA and rowB of a width-cols row-major array, in place.

def CompPoly.DenseMatrix.scaleRowData {F : Type u_1} [Field F] (cols row : ℕ) (factor : F) (data : Array F) : Array F

Scale row row of a width-cols row-major array by factor, in place.

def CompPoly.DenseMatrix.addScaledRowData {F : Type u_1} [Field F] (cols target source : ℕ) (factor : F) (data : Array F) : Array F

Add factor times row source to row target (with target ≠ source), in place.

def CompPoly.DenseMatrix.findPivotRowData {F : Type u_1} [Zero F] [BEq F] (rows cols startRow col : ℕ) (data : Array F) : Option ℕ

Find a pivot row at or below startRow in column col.

def CompPoly.DenseMatrix.normalizeAndEliminateData {F : Type u_1} [Field F] [BEq F] (rows cols pivotRow pivotCol : ℕ) (data : Array F) : Array F

Normalize the pivot row and clear the pivot column in every other row, in place.

def CompPoly.DenseMatrix.rrefLoopData {F : Type u_1} [Field F] [BEq F] : ℕ → ℕ → ℕ → ℕ → ℕ → Array F → Array ℕ → Array F × Array ℕ

Fuel-bounded Gauss-Jordan reduction over a bare row-major array.

def CompPoly.DenseMatrix.rrefInPlace {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) : RrefResult F

Reduced row-echelon form with pivot-column metadata, computed in place.

This destructures M so the backing array is owned by the reduction loop rather than aliased through the structure, which is what lets setIfInBounds mutate in place. The result equals rref M.

def CompPoly.DenseMatrix.homogeneousKernelBasisInPlace {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) : Array (Array F)

Homogeneous kernel basis extracted from the in-place RREF free columns.

def CompPoly.DenseMatrix.homogeneousWitnessInPlace {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) : Option (Array F)

One nonzero homogeneous-kernel witness via in-place reduction, if a free column exists. Output-identical to homogeneousWitness.