Row-span API over the echelon contracts.

The IsEchelonForm section transports row combinations across the echelon transform and builds the decidable row-span tests spanCoeffs/spanContains with their soundness lemmas. The IsRowReduced section adds the helper theory (pivot-column structure, single-row combinations) and proves the tests complete (spanCoeffs_complete, spanContains_iff).

theorem Hex.Matrix.IsEchelonForm.vecMul_transform_transpose {R : Type u} {n m : Nat} [Lean.Grind.CommRing R] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsEchelonForm D) (e : Vector R n) : vecMul (D.transform.transpose * e) M = vecMul e D.echelon

Row combinations transport forward along the echelon transform.

theorem Hex.Matrix.IsEchelonForm.vecMul_transformInv_transpose {R : Type u} {n m : Nat} [Lean.Grind.CommRing R] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsEchelonForm D) {Tinv : Matrix R n n} (hTinv : Tinv * D.transform = Matrix.identity n) (c : Vector R n) : vecMul (Tinv.transpose * c) D.echelon = vecMul c M

Converse row-combination transport: an M-row-combination witness c yields a D.echelon-row-combination witness Matrix.transpose Tinv * c, where Tinv is any left inverse of D.transform. The proof reuses the forward transport at the candidate witness.

theorem Hex.Matrix.IsEchelonForm.exists_vecMul_echelon_of_M {R : Type u} {n m : Nat} [Lean.Grind.CommRing R] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsEchelonForm D) {v : Vector R m} (h : ∃ (c : Vector R n), vecMul c M = v) : ∃ (d : Vector R n), vecMul d D.echelon = v

Existential converse transport: any v in the row span of M is also in the row span of D.echelon, with an explicit witness produced from a left inverse of D.transform.

def Hex.Matrix.IsEchelonForm.echelonCoeffs {R : Type u} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} [Lean.Grind.Field R] (E : M.IsEchelonForm D) (v : Vector R m) : Vector R n

The echelon-side coefficients selected by pivot coordinates.

Equations

• E.echelonCoeffs v = Vector.ofFn fun (i : Fin n) => if h : ↑i < D.rank then let pi := ⟨↑i, h⟩; v[D.pivotCols.get pi] / D.echelon[(E.pivotRow pi, D.pivotCols.get pi)] else 0

def Hex.Matrix.IsEchelonForm.spanCoeffs {R : Type u} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} [Lean.Grind.Field R] [DecidableEq R] (E : M.IsEchelonForm D) (v : Vector R m) : Option (Vector R n)

Coefficients for expressing v in the row span, if the echelon rows solve it.

Equations

• E.spanCoeffs v = if Hex.Matrix.vecMul (D.transform.transpose * E.echelonCoeffs v) M = v then some (D.transform.transpose * E.echelonCoeffs v) else none

def Hex.Matrix.IsEchelonForm.spanContains {R : Type u} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} [Lean.Grind.Field R] [DecidableEq R] (E : M.IsEchelonForm D) (v : Vector R m) : Bool

Decidable row-span membership test derived from spanCoeffs.

Equations

• E.spanContains v = (E.spanCoeffs v).isSome

@[simp]

theorem Hex.Matrix.IsEchelonForm.spanContains_eq_isSome {R : Type u} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} [Lean.Grind.Field R] [DecidableEq R] (E : M.IsEchelonForm D) (v : Vector R m) : E.spanContains v = (E.spanCoeffs v).isSome

spanContains is the Boolean isSome view of spanCoeffs.

theorem Hex.Matrix.IsEchelonForm.spanCoeffs_sound {R : Type u} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} [Lean.Grind.Field R] [DecidableEq R] (E : M.IsEchelonForm D) (v : Vector R m) (c : Vector R n) : E.spanCoeffs v = some c → vecMul c M = v

spanCoeffs returns coefficients whose row combination equals v.

theorem Hex.Matrix.IsEchelonForm.spanContains_sound {R : Type u} {n m : Nat} [Mul R] [Add R] [OfNat R 0] [OfNat R 1] {M : Matrix R n m} {D : RowEchelonData R n m} [Lean.Grind.Field R] [DecidableEq R] (E : M.IsEchelonForm D) (v : Vector R m) : E.spanContains v = true → ∃ (c : Vector R n), vecMul c M = v

If spanContains succeeds, the vector is in the row span.

theorem Hex.Matrix.IsRowReduced.hasNonzeroPivots {R : Type u} {n m : Nat} [Lean.Grind.Field R] {M : Matrix R n m} {D : RowEchelonData R n m} (E : M.IsRowReduced D) : ⋯.HasNonzeroPivots

RREF data has nonzero pivots because every pivot is normalized to one.

theorem Hex.Matrix.IsRowReduced.vecMul_single {R : Type u} [Lean.Grind.CommRing R] {n m : Nat} (M : Matrix R n m) (i : Fin n) : vecMul (Vector.ofFn fun (l : Fin n) => if i = l then 1 else 0) M = M.row i

A row-combination vector with a single coefficient 1 at row i and zero elsewhere selects exactly row i of the matrix. This packages the singleton-row case used by span and RREF arguments.

theorem Hex.Matrix.IsRowReduced.spanCoeffs_complete {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Lean.Grind.Field R] [DecidableEq R] (E : M.IsRowReduced D) (v : Vector R m) : (∃ (c : Vector R n), vecMul c M = v) → (⋯.spanCoeffs v).isSome = true

Any vector in the row span produces coefficients via the RREF-backed spanCoeffs API.

theorem Hex.Matrix.IsRowReduced.spanContains_iff {R : Type u} {n m : Nat} {M : Matrix R n m} {D : RowEchelonData R n m} [Lean.Grind.Field R] [DecidableEq R] (E : M.IsRowReduced D) (v : Vector R m) : ⋯.spanContains v = true ↔ ∃ (c : Vector R n), vecMul c M = v

For RREF data, spanContains is exactly row-span membership.