Gaussian elimination: single forward-elimination pivot step (refinement)

This file records one forward-elimination pivot step of Gaussian elimination as a refinement statement on the Mathlib Matrix representation, and proves the property the whole elimination relies on: the step preserves the solution set of the linear system A · x = b.

A forward-elimination pivot step toward eliminating column entry r against pivot row p replaces

• row r of the coefficient matrix A with row r − c • row p, and
• the target entry b r with b r − c • b p,

leaving every other row and target entry untouched. Because the modified r-equation is exactly (original r-equation) − c · (original p-equation) and the p-equation is unchanged, a vector x satisfies the new system iff it satisfies the original one. That single-step solution-set invariance is what the full elimination iterates.

This is the CoqEAL linear-solve / Gaussian-elimination tail flagged as a residual in SeqMatrixMul.lean. Here we discharge the single pivot step; the full forward sweep (choosing pivots, iterating over all rows, and the back-substitution / termination argument) is the named residual and is not attempted.

API

• pivotStepMat — the coefficient matrix after one pivot step.
• pivotStepRhs — the target vector after one pivot step.
• pivotStep_preserves_solution — x solves the stepped system iff it solves the original one (the solution-set invariance).

def Transfer.Examples.CoqEAL.GaussPivotStep.pivotStepMat {n : Type u_1} [DecidableEq n] {R : Type u_2} [CommRing R] (A : Matrix n n R) (p r : n) (c : R) : Matrix n n R

The coefficient matrix after one forward-elimination pivot step: row r is replaced by row r − c • row p; all other rows are unchanged.

Equations

• Transfer.Examples.CoqEAL.GaussPivotStep.pivotStepMat A p r c = A.updateRow r (A r - c • A p)

def Transfer.Examples.CoqEAL.GaussPivotStep.pivotStepRhs {n : Type u_1} [DecidableEq n] {R : Type u_2} [CommRing R] (b : n → R) (p r : n) (c : R) : n → R

The target vector after one forward-elimination pivot step: entry r is replaced by b r − c • b p; all other entries are unchanged.

Equations

• Transfer.Examples.CoqEAL.GaussPivotStep.pivotStepRhs b p r c = Function.update b r (b r - c • b p)

theorem Transfer.Examples.CoqEAL.GaussPivotStep.pivotStepMat_mulVec_ne {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (A : Matrix n n R) (p r : n) (c : R) (x : n → R) {i : n} (hi : i ≠ r) : (pivotStepMat A p r c).mulVec x i = A.mulVec x i

Off-pivot rows are unchanged by the step: for i ≠ r, the i-th equation of the stepped system is the i-th equation of the original.

theorem Transfer.Examples.CoqEAL.GaussPivotStep.pivotStepMat_mulVec_self {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (A : Matrix n n R) (p r : n) (c : R) (x : n → R) : (pivotStepMat A p r c).mulVec x r = A.mulVec x r - c • A.mulVec x p

The pivot row r of the stepped system is the original r-equation minus c times the original p-equation.

theorem Transfer.Examples.CoqEAL.GaussPivotStep.pivotStep_preserves_solution {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (A : Matrix n n R) (b : n → R) (p r : n) (c : R) (hpr : p ≠ r) (x : n → R) : (pivotStepMat A p r c).mulVec x = pivotStepRhs b p r c ↔ A.mulVec x = b

Single pivot step preserves the solution set. A vector x satisfies the stepped system pivotStepMat A p r c · x = pivotStepRhs b p r c iff it satisfies the original system A · x = b. This is the solution-set invariance that the full Gaussian forward sweep iterates.