In-Place Dense Kernel Correctness

The in-place homogeneous-kernel backend (KernelInPlace.lean) performs the same arithmetic, in the same order, as the copying backend (RowOps.lean/Kernel.lean), so it returns the same witness. This file proves that equivalence, culminating in homogeneousWitnessInPlace_eq, which lets the certified Guruswami-Sudan backend run the in-place implementation while reusing every existing correctness theorem.

theorem CompPoly.DenseMatrix.scaleRowData_eq {F : Type u_1} [Field F] (M : DenseMatrix F) (r : ℕ) (factor : F) : scaleRowData M.cols r factor M.data = (M.scaleRow r factor).data

The in-place scale of a row produces the same backing array as the copying scale.

theorem CompPoly.DenseMatrix.addScaledRowData_eq {F : Type u_1} [Field F] (M : DenseMatrix F) (target source : ℕ) (factor : F) (hts : target ≠ source) : addScaledRowData M.cols target source factor M.data = (M.addScaledRow target source factor).data

The in-place add-scaled row produces the same backing array as the copying version, when the target and source rows are distinct.

theorem CompPoly.DenseMatrix.swapRowsData_eq {F : Type u_1} [Zero F] (M : DenseMatrix F) (rowA rowB : ℕ) : swapRowsData M.cols rowA rowB M.data = (M.swapRows rowA rowB).data

The in-place row swap produces the same backing array as the copying swap.

theorem CompPoly.DenseMatrix.findPivotRowData_eq {F : Type u_1} [Zero F] [BEq F] (M : DenseMatrix F) (startRow col : ℕ) : findPivotRowData M.rows M.cols startRow col M.data = M.findPivotRow startRow col

The in-place pivot search agrees with the copying one.

theorem CompPoly.DenseMatrix.normalizeAndEliminateData_eq {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) (pivotRow pivotCol : ℕ) : normalizeAndEliminateData M.rows M.cols pivotRow pivotCol M.data = (M.normalizeAndEliminate pivotRow pivotCol).data

The in-place normalize-and-eliminate step produces the same backing array.

theorem CompPoly.DenseMatrix.rrefLoopData_eq {F : Type u_1} [Field F] [BEq F] (fuel col row : ℕ) (M : DenseMatrix F) (pivots : Array ℕ) : rrefLoopData fuel M.rows M.cols col row M.data pivots = ((rrefLoop fuel col row M pivots).matrix.data, (rrefLoop fuel col row M pivots).pivots)

The in-place reduction loop tracks the copying reduction loop, returning the same reduced backing array and the same pivot columns.

theorem CompPoly.DenseMatrix.rrefInPlace_eq {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) : M.rrefInPlace = M.rref

The in-place RREF equals the copying RREF.

theorem CompPoly.DenseMatrix.homogeneousWitnessInPlace_eq {F : Type u_1} [Field F] [BEq F] (M : DenseMatrix F) : M.homogeneousWitnessInPlace = M.homogeneousWitness

The in-place homogeneous-kernel witness equals the copying witness.